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

Metamath Proof Explorer

Theorem hash2exprb

Description: A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018)

Ref Expression
Assertion hash2exprb 
|- ( V e. W -> ( ( # ` V ) = 2 <-> E. a E. b ( a =/= b /\ V = { a , b } ) ) )

Proof

Step Hyp Ref Expression
1 hash2prde 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> E. a E. b ( a =/= b /\ V = { a , b } ) )
2 1 ex 
 |-  ( V e. W -> ( ( # ` V ) = 2 -> E. a E. b ( a =/= b /\ V = { a , b } ) ) )
3 hashprg 
 |-  ( ( a e. _V /\ b e. _V ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
4 3 el2v 
 |-  ( a =/= b <-> ( # ` { a , b } ) = 2 )
5 4 a1i 
 |-  ( V = { a , b } -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
6 5 biimpd 
 |-  ( V = { a , b } -> ( a =/= b -> ( # ` { a , b } ) = 2 ) )
7 fveqeq2 
 |-  ( V = { a , b } -> ( ( # ` V ) = 2 <-> ( # ` { a , b } ) = 2 ) )
8 6 7 sylibrd 
 |-  ( V = { a , b } -> ( a =/= b -> ( # ` V ) = 2 ) )
9 8 impcom 
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( # ` V ) = 2 )
10 9 a1i 
 |-  ( V e. W -> ( ( a =/= b /\ V = { a , b } ) -> ( # ` V ) = 2 ) )
11 10 exlimdvv 
 |-  ( V e. W -> ( E. a E. b ( a =/= b /\ V = { a , b } ) -> ( # ` V ) = 2 ) )
12 2 11 impbid 
 |-  ( V e. W -> ( ( # ` V ) = 2 <-> E. a E. b ( a =/= b /\ V = { a , b } ) ) )