x:A. 
B(x) 
B'(x)) 
({x:A| B(x) } ~ {x:A| B'(x) })x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) })B(x) } ~ {x:A| B(x) }| Rank | Theorem | Name |
| 5 | x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred] |
| cites the following: | ||
| 2 | x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred2] |
| 4 | B(x) } ~ {x:A| B(x) } | [subset_sq_remove_card] |