Theorem preqsnd 4859

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 481	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐴 ∈ 𝑉)
3		preqsnd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	adantl 481	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐵 ∈ 𝑊)
5		simpl 482	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐶 ∈ V)
6		dfsn2 4639	. . . . 5 ⊢ {𝐶} = {𝐶, 𝐶}
7	6	eqeq2i 2750	. . . 4 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐶})
8		preq12bg 4853	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))))
9		oridm 905	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))
10	8, 9	bitrdi 287	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
11	7, 10	bitrid 283	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
12	2, 4, 5, 5, 11	syl22anc 839	. 2 ⊢ ((𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
13		snprc 4717	. . . . . . 7 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
14	13	biimpi 216	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → {𝐶} = ∅)
15	14	adantr 480	. . . . 5 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → {𝐶} = ∅)
16	15	eqeq2d 2748	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = ∅))
17		prnzg 4778	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
18		eqneqall 2951	. . . . . . 7 ⊢ ({𝐴, 𝐵} = ∅ → ({𝐴, 𝐵} ≠ ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
19	17, 18	syl5com 31	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
20	1, 19	syl 17	. . . . 5 ⊢ (𝜑 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
21	20	adantl 481	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
22	16, 21	sylbid 240	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
23		eleq1 2829	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
24	23	eqcoms 2745	. . . . . . . . 9 ⊢ (𝐴 = 𝐶 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
25	24	notbid 318	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V))
26		pm2.24 124	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
27		elex 3501	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
28	26, 27	syl11 33	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
29	25, 28	biimtrdi 253	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
30	29	com13 88	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
31	1, 30	syl 17	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
32	31	impcom 407	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
33	32	impd 410	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶}))
34	22, 33	impbid 212	. 2 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
35	12, 34	pm2.61ian 812	1 ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480  ∅c0 4333  {csn 4626  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-pr 4629

This theorem is referenced by:  prnesn  4860  preqsn  4862  opeqsng  5508  1loopgrnb0  29520  disjdifprg  32588