Theorem preqsnd 4791

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 484	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐴 ∈ V)
3		preqsnd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
4	3	adantl 484	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐵 ∈ V)
5		simpl 485	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐶 ∈ V)
6		dfsn2 4582	. . . . 5 ⊢ {𝐶} = {𝐶, 𝐶}
7	6	eqeq2i 2836	. . . 4 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐶})
8		preq12bg 4786	. . . . 5 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))))
9		oridm 901	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))
10	8, 9	syl6bb 289	. . . 4 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
11	7, 10	syl5bb 285	. . 3 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
12	2, 4, 5, 5, 11	syl22anc 836	. 2 ⊢ ((𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
13		snprc 4655	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
14	13	biimpi 218	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
15	14	adantr 483	. . . . 5 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → {𝐶} = ∅)
16	15	eqeq2d 2834	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = ∅))
17		prnzg 4715	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝐴, 𝐵} ≠ ∅)
18		eqneqall 3029	. . . . . . 7 ⊢ ({𝐴, 𝐵} = ∅ → ({𝐴, 𝐵} ≠ ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
19	17, 18	syl5com 31	. . . . . 6 ⊢ (𝐴 ∈ V → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
21	20	adantl 484	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
22	16, 21	sylbid 242	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
23		eleq1 2902	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
24	23	eqcoms 2831	. . . . . . . . 9 ⊢ (𝐴 = 𝐶 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
25	24	notbid 320	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V))
26		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
27	25, 26	syl6bi 255	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V → (𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
28	27	com13 88	. . . . . 6 ⊢ (𝐴 ∈ V → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
29	1, 28	syl 17	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
30	29	impcom 410	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
31	30	impd 413	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶}))
32	22, 31	impbid 214	. 2 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
33	12, 32	pm2.61ian 810	1 ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  Vcvv 3496  ∅c0 4293  {csn 4569  {cpr 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-sn 4570  df-pr 4572

This theorem is referenced by:  prnesn  4792  preqsn  4794  opeqsng  5395  1loopgrnb0  27286  disjdifprg  30327