Theorem pr2ne

Description: If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)

	Ref	Expression
Assertion	pr2ne	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )

Proof

Step	Hyp	Ref	Expression
1		snnen2o	|- -. { A } ~~ 2o
2		dfsn2	|- { A } = { A , A }
3		preq2	|- ( A = B -> { A , A } = { A , B } )
4	2 3	eqtr2id	|- ( A = B -> { A , B } = { A } )
5	4	breq1d	|- ( A = B -> ( { A , B } ~~ 2o <-> { A } ~~ 2o ) )
6	1 5	mtbiri	|- ( A = B -> -. { A , B } ~~ 2o )
7	6	necon2ai	|- ( { A , B } ~~ 2o -> A =/= B )
8		enpr2	|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )
9	8	3expia	|- ( ( A e. C /\ B e. D ) -> ( A =/= B -> { A , B } ~~ 2o ) )
10	7 9	impbid2	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )