P(x) } =ext {x:A| P(x) }
x:A. B(x) 
B'(x)) 
({x:A| B(x) } =ext {x:A| B'(x) })P P| Rank | Theorem | Name |
| 3 | P(x) } =ext {x:A| P(x) } | [subset_squash_exteq] |
| cites the following: | ||
| 2 | x:A. B(x) B'(x)) ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_sq_exteq] |
| 0 | P P | [sq_sq_iff_sq] |