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