Theorem hashprb

Description: The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018)

	Ref	Expression
Assertion	hashprb	|- ( ( M e. _V /\ N e. _V /\ M =/= N ) <-> ( # ` { M , N } ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		hashprg	|- ( ( M e. _V /\ N e. _V ) -> ( M =/= N <-> ( # ` { M , N } ) = 2 ) )
2	1	biimp3a	|- ( ( M e. _V /\ N e. _V /\ M =/= N ) -> ( # ` { M , N } ) = 2 )
3		elprchashprn2	|- ( -. M e. _V -> -. ( # ` { M , N } ) = 2 )
4		pm2.21	|- ( -. ( # ` { M , N } ) = 2 -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
5	3 4	syl	|- ( -. M e. _V -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
6		elprchashprn2	|- ( -. N e. _V -> -. ( # ` { N , M } ) = 2 )
7		prcom	|- { N , M } = { M , N }
8	7	fveq2i	|- ( # ` { N , M } ) = ( # ` { M , N } )
9	8	eqeq1i	|- ( ( # ` { N , M } ) = 2 <-> ( # ` { M , N } ) = 2 )
10	9 4	sylnbi	|- ( -. ( # ` { N , M } ) = 2 -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
11	6 10	syl	|- ( -. N e. _V -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
12		simpll	|- ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> M e. _V )
13		simplr	|- ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> N e. _V )
14	1	biimpar	|- ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> M =/= N )
15	12 13 14	3jca	|- ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> ( M e. _V /\ N e. _V /\ M =/= N ) )
16	15	ex	|- ( ( M e. _V /\ N e. _V ) -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
17	5 11 16	ecase	|- ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) )
18	2 17	impbii	|- ( ( M e. _V /\ N e. _V /\ M =/= N ) <-> ( # ` { M , N } ) = 2 )