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
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) ) )

Proof

Step Hyp Ref Expression
1 dfopg
 |-  ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2 1 eqeq1d
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = { C } <-> { { A } , { A , B } } = { C } ) )
3 snex
 |-  { A } e. _V
4 prex
 |-  { A , B } e. _V
5 3 4 preqsn
 |-  ( { { A } , { A , B } } = { C } <-> ( { A } = { A , B } /\ { A , B } = C ) )
6 5 a1i
 |-  ( ( A e. V /\ B e. W ) -> ( { { A } , { A , B } } = { C } <-> ( { A } = { A , B } /\ { A , B } = C ) ) )
7 eqcom
 |-  ( { A } = { A , B } <-> { A , B } = { A } )
8 simpl
 |-  ( ( A e. V /\ B e. W ) -> A e. V )
9 simpr
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
10 8 9 preqsnd
 |-  ( ( A e. V /\ B e. W ) -> ( { A , B } = { A } <-> ( A = A /\ B = A ) ) )
11 simpr
 |-  ( ( A = A /\ B = A ) -> B = A )
12 eqid
 |-  A = A
13 12 jctl
 |-  ( B = A -> ( A = A /\ B = A ) )
14 11 13 impbii
 |-  ( ( A = A /\ B = A ) <-> B = A )
15 eqcom
 |-  ( B = A <-> A = B )
16 14 15 bitri
 |-  ( ( A = A /\ B = A ) <-> A = B )
17 10 16 bitrdi
 |-  ( ( A e. V /\ B e. W ) -> ( { A , B } = { A } <-> A = B ) )
18 7 17 syl5bb
 |-  ( ( A e. V /\ B e. W ) -> ( { A } = { A , B } <-> A = B ) )
19 18 anbi1d
 |-  ( ( A e. V /\ B e. W ) -> ( ( { A } = { A , B } /\ { A , B } = C ) <-> ( A = B /\ { A , B } = C ) ) )
20 dfsn2
 |-  { A } = { A , A }
21 preq2
 |-  ( A = B -> { A , A } = { A , B } )
22 20 21 eqtr2id
 |-  ( A = B -> { A , B } = { A } )
23 22 eqeq1d
 |-  ( A = B -> ( { A , B } = C <-> { A } = C ) )
24 eqcom
 |-  ( { A } = C <-> C = { A } )
25 23 24 bitrdi
 |-  ( A = B -> ( { A , B } = C <-> C = { A } ) )
26 25 a1i
 |-  ( ( A e. V /\ B e. W ) -> ( A = B -> ( { A , B } = C <-> C = { A } ) ) )
27 26 pm5.32d
 |-  ( ( A e. V /\ B e. W ) -> ( ( A = B /\ { A , B } = C ) <-> ( A = B /\ C = { A } ) ) )
28 19 27 bitrd
 |-  ( ( A e. V /\ B e. W ) -> ( ( { A } = { A , B } /\ { A , B } = C ) <-> ( A = B /\ C = { A } ) ) )
29 2 6 28 3bitrd
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) ) )