Theorem dcdifsnid 6715

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 3824 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 3824	. . 3 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
2	1	adantl 277	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3		simpr 110	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4		velsn 3690	. . . . . . 7 ⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
5	3, 4	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6		elun2 3377	. . . . . 6 ⊢ (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
7	5, 6	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8		simplr 529	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ 𝐴)
9		simpr 110	. . . . . . . 8 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
10	9, 4	sylnibr 684	. . . . . . 7 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
11	8, 10	eldifd 3211	. . . . . 6 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12		elun1 3376	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
13	11, 12	syl 14	. . . . 5 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14		simpll 527	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
15		simpr 110	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
16		simplr 529	. . . . . . . 8 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝐴)
17		equequ1 1760	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
18	17	dcbid 846	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑧 = 𝑦))
19		eqeq2 2241	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (𝑧 = 𝑦 ↔ 𝑧 = 𝐵))
20	19	dcbid 846	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦 ↔ DECID 𝑧 = 𝐵))
21	18, 20	rspc2v 2924	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
22	15, 16, 21	syl2anc 411	. . . . . . 7 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵))
23	14, 22	mpd 13	. . . . . 6 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → DECID 𝑧 = 𝐵)
24		exmiddc 844	. . . . . 6 ⊢ (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
25	23, 24	syl 14	. . . . 5 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
26	7, 13, 25	mpjaodan 806	. . . 4 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
27	26	ex 115	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → (𝑧 ∈ 𝐴 → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
28	27	ssrdv 3234	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
29	2, 28	eqssd 3245	1 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842   = wceq 1398   ∈ wcel 2202  ∀wral 2511   ∖ cdif 3198   ∪ cun 3199   ⊆ wss 3201  {csn 3673

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-dc 843  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679

This theorem is referenced by:  fnsnsplitdc  6716  nndifsnid  6718  fidifsnid  7101  undifdc  7159