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