Theorem difsnen 8794

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

Assertion

Ref	Expression
difsnen	⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))

Proof of Theorem difsnen

Step	Hyp	Ref	Expression
1		difexg 5246	. . . . . 6 ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∖ {𝐴}) ∈ V)
2		enrefg 8727	. . . . . 6 ⊢ ((𝑋 ∖ {𝐴}) ∈ V → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐴}))
3	1, 2	syl 17	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐴}))
4	3	3ad2ant1 1131	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐴}))
5		sneq 4568	. . . . . 6 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
6	5	difeq2d 4053	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑋 ∖ {𝐴}) = (𝑋 ∖ {𝐵}))
7	6	breq2d 5082	. . . 4 ⊢ (𝐴 = 𝐵 → ((𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐴}) ↔ (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})))
8	4, 7	syl5ibcom 244	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})))
9	8	imp 406	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 = 𝐵) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
10		simpl1 1189	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝑋 ∈ 𝑉)
11		difexg 5246	. . . . . 6 ⊢ ((𝑋 ∖ {𝐴}) ∈ V → ((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∈ V)
12		enrefg 8727	. . . . . 6 ⊢ (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∈ V → ((𝑋 ∖ {𝐴}) ∖ {𝐵}) ≈ ((𝑋 ∖ {𝐴}) ∖ {𝐵}))
13	10, 1, 11, 12	4syl 19	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝑋 ∖ {𝐴}) ∖ {𝐵}) ≈ ((𝑋 ∖ {𝐴}) ∖ {𝐵}))
14		dif32 4223	. . . . 5 ⊢ ((𝑋 ∖ {𝐴}) ∖ {𝐵}) = ((𝑋 ∖ {𝐵}) ∖ {𝐴})
15	13, 14	breqtrdi 5111	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝑋 ∖ {𝐴}) ∖ {𝐵}) ≈ ((𝑋 ∖ {𝐵}) ∖ {𝐴}))
16		simpl3 1191	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑋)
17		simpl2 1190	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑋)
18		en2sn 8785	. . . . 5 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → {𝐵} ≈ {𝐴})
19	16, 17, 18	syl2anc 583	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → {𝐵} ≈ {𝐴})
20		disjdifr 4403	. . . . 5 ⊢ (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∩ {𝐵}) = ∅
21	20	a1i 11	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∩ {𝐵}) = ∅)
22		disjdifr 4403	. . . . 5 ⊢ (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∩ {𝐴}) = ∅
23	22	a1i 11	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∩ {𝐴}) = ∅)
24		unen 8790	. . . 4 ⊢ (((((𝑋 ∖ {𝐴}) ∖ {𝐵}) ≈ ((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∧ {𝐵} ≈ {𝐴}) ∧ ((((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∩ {𝐵}) = ∅ ∧ (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∩ {𝐴}) = ∅)) → (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∪ {𝐵}) ≈ (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∪ {𝐴}))
25	15, 19, 21, 23, 24	syl22anc 835	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∪ {𝐵}) ≈ (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∪ {𝐴}))
26		simpr 484	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵)
27	26	necomd 2998	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐵 ≠ 𝐴)
28		eldifsn 4717	. . . . 5 ⊢ (𝐵 ∈ (𝑋 ∖ {𝐴}) ↔ (𝐵 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴))
29	16, 27, 28	sylanbrc 582	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ (𝑋 ∖ {𝐴}))
30		difsnid 4740	. . . 4 ⊢ (𝐵 ∈ (𝑋 ∖ {𝐴}) → (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∪ {𝐵}) = (𝑋 ∖ {𝐴}))
31	29, 30	syl 17	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝑋 ∖ {𝐴}) ∖ {𝐵}) ∪ {𝐵}) = (𝑋 ∖ {𝐴}))
32		eldifsn 4717	. . . . 5 ⊢ (𝐴 ∈ (𝑋 ∖ {𝐵}) ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵))
33	17, 26, 32	sylanbrc 582	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (𝑋 ∖ {𝐵}))
34		difsnid 4740	. . . 4 ⊢ (𝐴 ∈ (𝑋 ∖ {𝐵}) → (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∪ {𝐴}) = (𝑋 ∖ {𝐵}))
35	33, 34	syl 17	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝑋 ∖ {𝐵}) ∖ {𝐴}) ∪ {𝐴}) = (𝑋 ∖ {𝐵}))
36	25, 31, 35	3brtr3d 5101	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
37	9, 36	pm2.61dane 3031	1 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882  ∅c0 4253  {csn 4558   class class class wbr 5070   ≈ cen 8688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-en 8692

This theorem is referenced by:  domdifsn  8795  domunsncan  8812  enfixsn  8821  infdifsn  9345  dju1dif  9859