Metamath Proof Explorer

Theorem difsnen

Description: All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion difsnen ⊢X∈V∧A∈X∧B∈X→X∖A≈X∖B

Proof

Step Hyp Ref Expression
1 difexg ⊢X∈V→X∖A∈V
2 enrefg ⊢X∖A∈V→X∖A≈X∖A
3 1 2 syl ⊢X∈V→X∖A≈X∖A
4 3 3ad2ant1 ⊢X∈V∧A∈X∧B∈X→X∖A≈X∖A
5 sneq ⊢A=B→A=B
6 5 difeq2d ⊢A=B→X∖A=X∖B
7 6 breq2d ⊢A=B→X∖A≈X∖A↔X∖A≈X∖B
8 4 7 syl5ibcom ⊢X∈V∧A∈X∧B∈X→A=B→X∖A≈X∖B
9 8 imp ⊢X∈V∧A∈X∧B∈X∧A=B→X∖A≈X∖B
10 simpl1 ⊢X∈V∧A∈X∧B∈X∧A≠B→X∈V
11 difexg ⊢X∖A∈V→X∖A∖B∈V
12 enrefg ⊢X∖A∖B∈V→X∖A∖B≈X∖A∖B
13 10 1 11 12 4syl ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A∖B≈X∖A∖B
14 dif32 ⊢X∖A∖B=X∖B∖A
15 13 14 breqtrdi ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A∖B≈X∖B∖A
16 simpl3 ⊢X∈V∧A∈X∧B∈X∧A≠B→B∈X
17 simpl2 ⊢X∈V∧A∈X∧B∈X∧A≠B→A∈X
18 en2sn ⊢B∈X∧A∈X→B≈A
19 16 17 18 syl2anc ⊢X∈V∧A∈X∧B∈X∧A≠B→B≈A
20 disjdifr ⊢X∖A∖B∩B=∅
21 20 a1i ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A∖B∩B=∅
22 disjdifr ⊢X∖B∖A∩A=∅
23 22 a1i ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖B∖A∩A=∅
24 unen ⊢X∖A∖B≈X∖B∖A∧B≈A∧X∖A∖B∩B=∅∧X∖B∖A∩A=∅→X∖A∖B∪B≈X∖B∖A∪A
25 15 19 21 23 24 syl22anc ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A∖B∪B≈X∖B∖A∪A
26 simpr ⊢X∈V∧A∈X∧B∈X∧A≠B→A≠B
27 26 necomd ⊢X∈V∧A∈X∧B∈X∧A≠B→B≠A
28 eldifsn ⊢B∈X∖A↔B∈X∧B≠A
29 16 27 28 sylanbrc ⊢X∈V∧A∈X∧B∈X∧A≠B→B∈X∖A
30 difsnid ⊢B∈X∖A→X∖A∖B∪B=X∖A
31 29 30 syl ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A∖B∪B=X∖A
32 eldifsn ⊢A∈X∖B↔A∈X∧A≠B
33 17 26 32 sylanbrc ⊢X∈V∧A∈X∧B∈X∧A≠B→A∈X∖B
34 difsnid ⊢A∈X∖B→X∖B∖A∪A=X∖B
35 33 34 syl ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖B∖A∪A=X∖B
36 25 31 35 3brtr3d ⊢X∈V∧A∈X∧B∈X∧A≠B→X∖A≈X∖B
37 9 36 pm2.61dane ⊢X∈V∧A∈X∧B∈X→X∖A≈X∖B