This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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