# Metamath Proof Explorer

## Theorem opeqsng

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.)

Ref Expression
Assertion opeqsng ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩=\left\{{C}\right\}↔\left({A}={B}\wedge {C}=\left\{{A}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfopg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to ⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$
2 1 eqeq1d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩=\left\{{C}\right\}↔\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}=\left\{{C}\right\}\right)$
3 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
4 prex ${⊢}\left\{{A},{B}\right\}\in \mathrm{V}$
5 3 4 preqsn ${⊢}\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}=\left\{{C}\right\}↔\left(\left\{{A}\right\}=\left\{{A},{B}\right\}\wedge \left\{{A},{B}\right\}={C}\right)$
6 5 a1i ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}=\left\{{C}\right\}↔\left(\left\{{A}\right\}=\left\{{A},{B}\right\}\wedge \left\{{A},{B}\right\}={C}\right)\right)$
7 eqcom ${⊢}\left\{{A}\right\}=\left\{{A},{B}\right\}↔\left\{{A},{B}\right\}=\left\{{A}\right\}$
8 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
9 8 adantr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {A}\in \mathrm{V}$
10 elex ${⊢}{B}\in {W}\to {B}\in \mathrm{V}$
11 10 adantl ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {B}\in \mathrm{V}$
12 9 11 preqsnd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{{A},{B}\right\}=\left\{{A}\right\}↔\left({A}={A}\wedge {B}={A}\right)\right)$
13 simpr ${⊢}\left({A}={A}\wedge {B}={A}\right)\to {B}={A}$
14 eqid ${⊢}{A}={A}$
15 14 jctl ${⊢}{B}={A}\to \left({A}={A}\wedge {B}={A}\right)$
16 13 15 impbii ${⊢}\left({A}={A}\wedge {B}={A}\right)↔{B}={A}$
17 eqcom ${⊢}{B}={A}↔{A}={B}$
18 16 17 bitri ${⊢}\left({A}={A}\wedge {B}={A}\right)↔{A}={B}$
19 12 18 syl6bb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{{A},{B}\right\}=\left\{{A}\right\}↔{A}={B}\right)$
20 7 19 syl5bb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{{A}\right\}=\left\{{A},{B}\right\}↔{A}={B}\right)$
21 20 anbi1d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left(\left\{{A}\right\}=\left\{{A},{B}\right\}\wedge \left\{{A},{B}\right\}={C}\right)↔\left({A}={B}\wedge \left\{{A},{B}\right\}={C}\right)\right)$
22 dfsn2 ${⊢}\left\{{A}\right\}=\left\{{A},{A}\right\}$
23 preq2 ${⊢}{A}={B}\to \left\{{A},{A}\right\}=\left\{{A},{B}\right\}$
24 22 23 syl5req ${⊢}{A}={B}\to \left\{{A},{B}\right\}=\left\{{A}\right\}$
25 24 eqeq1d ${⊢}{A}={B}\to \left(\left\{{A},{B}\right\}={C}↔\left\{{A}\right\}={C}\right)$
26 eqcom ${⊢}\left\{{A}\right\}={C}↔{C}=\left\{{A}\right\}$
27 25 26 syl6bb ${⊢}{A}={B}\to \left(\left\{{A},{B}\right\}={C}↔{C}=\left\{{A}\right\}\right)$
28 27 a1i ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}={B}\to \left(\left\{{A},{B}\right\}={C}↔{C}=\left\{{A}\right\}\right)\right)$
29 28 pm5.32d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}={B}\wedge \left\{{A},{B}\right\}={C}\right)↔\left({A}={B}\wedge {C}=\left\{{A}\right\}\right)\right)$
30 21 29 bitrd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left(\left\{{A}\right\}=\left\{{A},{B}\right\}\wedge \left\{{A},{B}\right\}={C}\right)↔\left({A}={B}\wedge {C}=\left\{{A}\right\}\right)\right)$
31 2 6 30 3bitrd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩=\left\{{C}\right\}↔\left({A}={B}\wedge {C}=\left\{{A}\right\}\right)\right)$