Metamath Proof Explorer

Theorem hash2prb

Description: A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 hash2exprb 
 |-  ( V e. W -> ( ( # ` V ) = 2 <-> E. a E. b ( a =/= b /\ V = { a , b } ) ) )
2 vex 
 |-  a e. _V
3 2 prid1 
 |-  a e. { a , b }
4 vex 
 |-  b e. _V
5 4 prid2 
 |-  b e. { a , b }
6 3 5 pm3.2i 
 |-  ( a e. { a , b } /\ b e. { a , b } )
7 eleq2 
 |-  ( V = { a , b } -> ( a e. V <-> a e. { a , b } ) )
8 eleq2 
 |-  ( V = { a , b } -> ( b e. V <-> b e. { a , b } ) )
9 7 8 anbi12d 
 |-  ( V = { a , b } -> ( ( a e. V /\ b e. V ) <-> ( a e. { a , b } /\ b e. { a , b } ) ) )
10 6 9 mpbiri 
 |-  ( V = { a , b } -> ( a e. V /\ b e. V ) )
11 10 adantl 
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( a e. V /\ b e. V ) )
12 11 pm4.71ri 
 |-  ( ( a =/= b /\ V = { a , b } ) <-> ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) )
13 12 2exbii 
 |-  ( E. a E. b ( a =/= b /\ V = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) )
14 13 a1i 
 |-  ( V e. W -> ( E. a E. b ( a =/= b /\ V = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) ) )
15 r2ex 
 |-  ( E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) )
16 15 bicomi 
 |-  ( E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) <-> E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) )
17 16 a1i 
 |-  ( V e. W -> ( E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ V = { a , b } ) ) <-> E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) ) )
18 1 14 17 3bitrd 
 |-  ( V e. W -> ( ( # ` V ) = 2 <-> E. a e. V E. b e. V ( a =/= b /\ V = { a , b } ) ) )