Theorem opeqsng 5358

Description: Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.)

Assertion

Ref	Expression
opeqsng	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))

Proof of Theorem opeqsng

Step	Hyp	Ref	Expression
1		dfopg 4761	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2	1	eqeq1d 2800	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = {𝐶} ↔ {{𝐴}, {𝐴, 𝐵}} = {𝐶}))
3		snex 5297	. . . 4 ⊢ {𝐴} ∈ V
4		prex 5298	. . . 4 ⊢ {𝐴, 𝐵} ∈ V
5	3, 4	preqsn 4752	. . 3 ⊢ ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶))
6	5	a1i 11	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶)))
7		eqcom 2805	. . . . 5 ⊢ ({𝐴} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴})
8		elex 3459	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
9	8	adantr 484	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ V)
10		elex 3459	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
11	10	adantl 485	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ V)
12	9, 11	preqsnd 4749	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} = {𝐴} ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐴)))
13		simpr 488	. . . . . . . 8 ⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) → 𝐵 = 𝐴)
14		eqid 2798	. . . . . . . . 9 ⊢ 𝐴 = 𝐴
15	14	jctl 527	. . . . . . . 8 ⊢ (𝐵 = 𝐴 → (𝐴 = 𝐴 ∧ 𝐵 = 𝐴))
16	13, 15	impbii 212	. . . . . . 7 ⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) ↔ 𝐵 = 𝐴)
17		eqcom 2805	. . . . . . 7 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
18	16, 17	bitri 278	. . . . . 6 ⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) ↔ 𝐴 = 𝐵)
19	12, 18	syl6bb 290	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} = {𝐴} ↔ 𝐴 = 𝐵))
20	7, 19	syl5bb 286	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} = {𝐴, 𝐵} ↔ 𝐴 = 𝐵))
21	20	anbi1d 632	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶)))
22		dfsn2 4538	. . . . . . . 8 ⊢ {𝐴} = {𝐴, 𝐴}
23		preq2 4630	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
24	22, 23	syl5req 2846	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2800	. . . . . 6 ⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ {𝐴} = 𝐶))
26		eqcom 2805	. . . . . 6 ⊢ ({𝐴} = 𝐶 ↔ 𝐶 = {𝐴})
27	25, 26	syl6bb 290	. . . . 5 ⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴}))
28	27	a1i 11	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴})))
29	28	pm5.32d 580	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))
30	21, 29	bitrd 282	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))
31	2, 6, 30	3bitrd 308	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {csn 4525  {cpr 4527  ⟨cop 4531

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  ax-sep 5167  ax-nul 5174  ax-pr 5295

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-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532

This theorem is referenced by:  opeqsn  5359  snopeqop  5361