x:A. 
B(x) 
B'(x)) 
({x:A| B(x) } =ext {x:A| B'(x) })x:A. B(x) B'(x)) {x:A| B(x) } 
{x:A| B'(x) }| Rank | Theorem | Name |
| 2 | x:A. B(x) B'(x)) ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_sq_exteq] |
| cites the following: | ||
| 1 | x:A. B(x) B'(x)) {x:A| B(x) } {x:A| B'(x) } | [set_inc_wrt_imp_sq] |