Theorem dcdifsnid 6303

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 3605 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 3605	. . 3 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
2	1	adantl 272	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3		simpr 109	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4		velsn 3483	. . . . . . 7 ⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
5	3, 4	sylibr 133	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6		elun2 3183	. . . . . 6 ⊢ (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
7	5, 6	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8		simplr 498	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ 𝐴)
9		simpr 109	. . . . . . . 8 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
10	9, 4	sylnibr 640	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
11	8, 10	eldifd 3023	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12		elun1 3182	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
13	11, 12	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14		simpll 497	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
15		simpr 109	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
16		simplr 498	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝐴)
17		equequ1 1652	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
18	17	dcbid 789	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑧 = 𝑦))
19		eqeq2 2104	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (𝑧 = 𝑦 ↔ 𝑧 = 𝐵))
20	19	dcbid 789	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦 ↔ DECID 𝑧 = 𝐵))
21	18, 20	rspc2v 2748	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
22	15, 16, 21	syl2anc 404	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
23	14, 22	mpd 13	. . . . . 6 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → DECID 𝑧 = 𝐵)
24		exmiddc 785	. . . . . 6 ⊢ (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
25	23, 24	syl 14	. . . . 5 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
26	7, 13, 25	mpjaodan 750	. . . 4 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
27	26	ex 114	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → (𝑧 ∈ 𝐴 → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
28	27	ssrdv 3045	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
29	2, 28	eqssd 3056	1 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 667  DECID wdc 783   = wceq 1296   ∈ wcel 1445  ∀wral 2370   ∖ cdif 3010   ∪ cun 3011   ⊆ wss 3013  {csn 3466

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-dc 784  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-v 2635  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472

This theorem is referenced by:  fnsnsplitdc  6304  nndifsnid  6306  fidifsnid  6667  undifdc  6714