This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( ( 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 } ) ) )