Theorem preqsnd 4749

Description: Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.) (Revised by AV, 13-Jun-2022.)

Hypotheses

Ref	Expression
preqsnd.1	⊢ (𝜑 → 𝐴 ∈ V)
preqsnd.2	⊢ (𝜑 → 𝐵 ∈ V)

Assertion

Ref	Expression
preqsnd	⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

Proof of Theorem preqsnd

Step	Hyp	Ref	Expression
1		preqsnd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
2	1	adantl 485	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐴 ∈ V)
3		preqsnd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
4	3	adantl 485	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐵 ∈ V)
5		simpl 486	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐶 ∈ V)
6		dfsn2 4538	. . . . 5 ⊢ {𝐶} = {𝐶, 𝐶}
7	6	eqeq2i 2811	. . . 4 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐶})
8		preq12bg 4744	. . . . 5 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))))
9		oridm 902	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))
10	8, 9	syl6bb 290	. . . 4 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
11	7, 10	syl5bb 286	. . 3 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
12	2, 4, 5, 5, 11	syl22anc 837	. 2 ⊢ ((𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
13		snprc 4613	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
14	13	biimpi 219	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
15	14	adantr 484	. . . . 5 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → {𝐶} = ∅)
16	15	eqeq2d 2809	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = ∅))
17		prnzg 4674	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝐴, 𝐵} ≠ ∅)
18		eqneqall 2998	. . . . . . 7 ⊢ ({𝐴, 𝐵} = ∅ → ({𝐴, 𝐵} ≠ ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
19	17, 18	syl5com 31	. . . . . 6 ⊢ (𝐴 ∈ V → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
21	20	adantl 485	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
22	16, 21	sylbid 243	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
23		eleq1 2877	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
24	23	eqcoms 2806	. . . . . . . . 9 ⊢ (𝐴 = 𝐶 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
25	24	notbid 321	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V))
26		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
27	25, 26	syl6bi 256	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V → (𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
28	27	com13 88	. . . . . 6 ⊢ (𝐴 ∈ V → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
29	1, 28	syl 17	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
30	29	impcom 411	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
31	30	impd 414	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶}))
32	22, 31	impbid 215	. 2 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
33	12, 32	pm2.61ian 811	1 ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441  ∅c0 4243  {csn 4525  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-sn 4526  df-pr 4528

This theorem is referenced by:  prnesn  4750  preqsn  4752  opeqsng  5358  1loopgrnb0  27292  disjdifprg  30338