Theorem preqsnd 4826

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

Hypotheses

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

Assertion

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

Proof of Theorem preqsnd

Step	Hyp	Ref	Expression
1		preqsnd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2	1	adantl 487	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐴 ∈ 𝑉)
3		preqsnd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	adantl 487	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐵 ∈ 𝑊)
5		simpl 488	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐶 ∈ V)
6		dfsn2 4604	. . . . 5 ⊢ {𝐶} = {𝐶, 𝐶}
7	6	eqeq2i 2778	. . . 4 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐶})
8		preq12bg 4820	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))))
9		oridm 918	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))
10	8, 9	bitrdi 290	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
11	7, 10	bitrid 286	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
12	2, 4, 5, 5, 11	syl22anc 852	. 2 ⊢ ((𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
13		snprc 4685	. . . . . 6 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
14	13	birani 509	. . . . 5 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → {𝐶} = ∅)
15	14	eqeq2d 2776	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = ∅))
16		prnzg 4746	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
17		eqneqall 2971	. . . . . . 7 ⊢ ({𝐴, 𝐵} = ∅ → ({𝐴, 𝐵} ≠ ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
18	16, 17	syl5com 32	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
19	1, 18	syl 18	. . . . 5 ⊢ (𝜑 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
20	19	adantl 487	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
21	15, 20	sylbid 243	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
22		eleq1 2853	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
23	22	eqcoms 2773	. . . . . . . . 9 ⊢ (𝐴 = 𝐶 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
24	23	notbid 321	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V))
25		pm2.24 125	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
26		elex 3478	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
27	25, 26	syl11 34	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
28	24, 27	biimtrdi 256	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
29	28	com13 89	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
30	1, 29	syl 18	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
31	30	impcom 413	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
32	31	impd 416	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶}))
33	21, 32	impbid 215	. 2 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
34	12, 33	pm2.61ian 824	1 ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  Vcvv 3457  ∅c0 4286  {csn 4591  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-pr 4594

This theorem is used by:  prnesn  4827  preqsn  4829  opeqsng  5488  1loopgrnb0  29881  disjdifprg  32949