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

Metamath Proof Explorer

Theorem funsneqopb

Description: A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Hypotheses funsndifnop.a 
|- A e. _V
funsndifnop.b 
|- B e. _V
funsndifnop.g 
|- G = { <. A , B >. }
Assertion funsneqopb 
|- ( A = B <-> G e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 funsndifnop.a 
 |-  A e. _V
2 funsndifnop.b 
 |-  B e. _V
3 funsndifnop.g 
 |-  G = { <. A , B >. }
4 opeq1 
 |-  ( A = B -> <. A , B >. = <. B , B >. )
5 4 sneqd 
 |-  ( A = B -> { <. A , B >. } = { <. B , B >. } )
6 2 snopeqopsnid 
 |-  { <. B , B >. } = <. { B } , { B } >.
7 5 6 eqtrdi 
 |-  ( A = B -> { <. A , B >. } = <. { B } , { B } >. )
8 3 7 eqtrid 
 |-  ( A = B -> G = <. { B } , { B } >. )
9 snex 
 |-  { B } e. _V
10 9 9 opelvv 
 |-  <. { B } , { B } >. e. ( _V X. _V )
11 8 10 eqeltrdi 
 |-  ( A = B -> G e. ( _V X. _V ) )
12 1 2 3 funsndifnop 
 |-  ( A =/= B -> -. G e. ( _V X. _V ) )
13 12 necon4ai 
 |-  ( G e. ( _V X. _V ) -> A = B )
14 11 13 impbii 
 |-  ( A = B <-> G e. ( _V X. _V ) )