x:A. Dec(
P(x))) 
(A ~ ({x:A| P(x) }+{x:A| 
P(x) }))B(x) } ~ {x:A| B(x) }(P) 
PP Px:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) }))| Rank | Theorem | Name |
| 5 | x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl_squash] |
| cites the following: | ||
| 4 | B(x) } ~ {x:A| B(x) } | [subset_sq_remove_card] |
| 0 | (P) P | [sq_not_iff_sq] |
| 0 | P P | [not_sq_iff_sq] |
| 3 | x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl] |