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) }| Theorem | Name |
| x:A. B(x) B'(x)) ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_exteq] |
| cites the following: | |
| x:A. B(x) B'(x)) {x:A| B(x) } {x:A| B'(x) } | [set_inc_wrt_imp] |