P:(A
Prop), B:(x:AType(given P(x))).
Thm* x:{u:A| P(u) }
B(x) =ext x:AB(x)(given P(x))B:(AProp), C:({u:A| B(u) }Type).
Thm* x:{u:A| B(u) }
C(x) =ext x:AC(x)(given B(x))P:(AProp). {x:A| P(x) }Prop =ext x:AProp(given P(x))| Theorem | Name |
| P:(AProp), B:(x:AType(given P(x))).
Thm* x:{u:A| P(u) } B(x) =ext x:AB(x)(given P(x)) | [sfa_doc_exteq_gfun2] |
| cites the following: | |
| B:(AProp), C:({u:A| B(u) }Type).
Thm* x:{u:A| B(u) } C(x) =ext x:AC(x)(given B(x)) | [sfa_doc_exteq_gfun] |
| P:(AProp). {x:A| P(x) }Prop =ext x:AProp(given P(x)) | [sfa_doc_exteq_gprop] |