Theorem dcdifsnid 6648

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 3813 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 3813	. . 3 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
2	1	adantl 277	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3		simpr 110	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4		velsn 3683	. . . . . . 7 ⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
5	3, 4	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6		elun2 3372	. . . . . 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 3207	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12		elun1 3371	. . . . . 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 2920	. . . . . . . 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 3230	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
29	2, 28	eqssd 3241	1 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

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

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 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672

This theorem is referenced by:  fnsnsplitdc  6649  nndifsnid  6651  fidifsnid  7029  undifdc  7082