Thm*
Thm* (
x:A. 
B(x) 
B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) })B(x) } ~ {x:A| B(x) }Thm*
Thm* (
x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) })| Rank | Theorem | Name |
| 5 | Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype_sq] |
| cites the following: | ||
| 4 | B(x) } ~ {x:A| B(x) } | [subset_sq_remove_card] |
| 1 | Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype] |