Theorem hashprdifel

Description: The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Hypothesis	hashprdifel.s	|- S = { A , B }
Assertion	hashprdifel	|- ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )

Proof

Step	Hyp	Ref	Expression
1		hashprdifel.s	|- S = { A , B }
2	1	fveq2i	|- ( # ` S ) = ( # ` { A , B } )
3	2	eqeq1i	|- ( ( # ` S ) = 2 <-> ( # ` { A , B } ) = 2 )
4		hashprb	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) <-> ( # ` { A , B } ) = 2 )
5	3 4	bitr4i	|- ( ( # ` S ) = 2 <-> ( A e. _V /\ B e. _V /\ A =/= B ) )
6		prid1g	|- ( A e. _V -> A e. { A , B } )
7	6	3ad2ant1	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. { A , B } )
8	7 1	eleqtrrdi	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. S )
9		prid2g	|- ( B e. _V -> B e. { A , B } )
10	9	3ad2ant2	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> B e. { A , B } )
11	10 1	eleqtrrdi	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> B e. S )
12		simp3	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A =/= B )
13	8 11 12	3jca	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> ( A e. S /\ B e. S /\ A =/= B ) )
14	5 13	sylbi	|- ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )