Theorem preqsnd 4797

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 482	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐴 ∈ 𝑉)
3		preqsnd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	adantl 482	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐵 ∈ 𝑊)
5		simpl 483	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝜑) → 𝐶 ∈ V)
6		dfsn2 4575	. . . . 5 ⊢ {𝐶} = {𝐶, 𝐶}
7	6	eqeq2i 2753	. . . 4 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐶})
8		preq12bg 4791	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))))
9		oridm 910	. . . . 5 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))
10	8, 9	bitrdi 288	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶, 𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
11	7, 10	bitrid 284	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ V ∧ 𝐶 ∈ V)) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
12	2, 4, 5, 5, 11	syl22anc 844	. 2 ⊢ ((𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
13		snprc 4656	. . . . . 6 ⊢ (¬ 𝐶 ∈ V ↔ {𝐶} = ∅)
14	13	birani 504	. . . . 5 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → {𝐶} = ∅)
15	14	eqeq2d 2751	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ {𝐴, 𝐵} = ∅))
16		prnzg 4717	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
17		eqneqall 2946	. . . . . . 7 ⊢ ({𝐴, 𝐵} = ∅ → ({𝐴, 𝐵} ≠ ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
18	16, 17	syl5com 31	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
19	1, 18	syl 17	. . . . 5 ⊢ (𝜑 → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
20	19	adantl 482	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = ∅ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
21	15, 20	sylbid 241	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
22		eleq1 2828	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
23	22	eqcoms 2748	. . . . . . . . 9 ⊢ (𝐴 = 𝐶 → (𝐶 ∈ V ↔ 𝐴 ∈ V))
24	23	notbid 319	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V))
25		pm2.24 124	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ V → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
26		elex 3453	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
27	25, 26	syl11 33	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
28	24, 27	biimtrdi 254	. . . . . . 7 ⊢ (𝐴 = 𝐶 → (¬ 𝐶 ∈ V → (𝐴 ∈ 𝑉 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
29	28	com13 88	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
30	1, 29	syl 17	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ V → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶}))))
31	30	impcom 408	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → (𝐴 = 𝐶 → (𝐵 = 𝐶 → {𝐴, 𝐵} = {𝐶})))
32	31	impd 411	. . 3 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶}))
33	21, 32	impbid 213	. 2 ⊢ ((¬ 𝐶 ∈ V ∧ 𝜑) → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
34	12, 33	pm2.61ian 817	1 ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  Vcvv 3432  ∅c0 4268  {csn 4562  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-nul 4269  df-sn 4563  df-pr 4565

This theorem is referenced by:  prnesn  4798  preqsn  4800  opeqsng  5451  1loopgrnb0  29596  disjdifprg  32671