Theorem dcdifsnid 6667

Description: If we remove a single element from a set with decidable equality then put it back in, we end up with the original set. This strengthens difsnss 3817 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)

Assertion

Ref	Expression
dcdifsnid	⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem dcdifsnid

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		difsnss 3817	. . 3 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
2	1	adantl 277	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3		simpr 110	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4		velsn 3684	. . . . . . 7 ⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
5	3, 4	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6		elun2 3373	. . . . . 6 ⊢ (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
7	5, 6	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8		simplr 528	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ 𝐴)
9		simpr 110	. . . . . . . 8 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
10	9, 4	sylnibr 681	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
11	8, 10	eldifd 3208	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12		elun1 3372	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
13	11, 12	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14		simpll 527	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
15		simpr 110	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
16		simplr 528	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝐴)
17		equequ1 1758	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
18	17	dcbid 843	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑧 = 𝑦))
19		eqeq2 2239	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (𝑧 = 𝑦 ↔ 𝑧 = 𝐵))
20	19	dcbid 843	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦 ↔ DECID 𝑧 = 𝐵))
21	18, 20	rspc2v 2921	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
22	15, 16, 21	syl2anc 411	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
23	14, 22	mpd 13	. . . . . 6 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → DECID 𝑧 = 𝐵)
24		exmiddc 841	. . . . . 6 ⊢ (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
25	23, 24	syl 14	. . . . 5 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
26	7, 13, 25	mpjaodan 803	. . . 4 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
27	26	ex 115	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → (𝑧 ∈ 𝐴 → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
28	27	ssrdv 3231	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
29	2, 28	eqssd 3242	1 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713  DECID wdc 839   = wceq 1395   ∈ wcel 2200  ∀wral 2508   ∖ cdif 3195   ∪ cun 3196   ⊆ wss 3198  {csn 3667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-dc 840  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673

This theorem is referenced by:  fnsnsplitdc  6668  nndifsnid  6670  fidifsnid  7053  undifdc  7109