B:(A
Type), P:(AProp).
Thm* (i:{i:A| P(i) }
B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) }B:(AType), P:(AProp).
Thm* (i:{i:A| P(i) }
B(i)) =ext {v:(i:AB(i))| P(v/x,y. x) }| Theorem | Name |
| B:(AType), P:(AProp).
Thm* (i:{i:A| P(i) } B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) } | [card_sigma_st_dom] |
| cites the following: | |
| B:(AType), P:(AProp).
Thm* (i:{i:A| P(i) } B(i)) =ext {v:(i:AB(i))| P(v/x,y. x) } | [exteq_sigma_st_dom] |