Metamath Proof Explorer


Theorem pren2

Description: An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 pr2ne
 |-  ( ( A e. _V /\ B e. _V ) -> ( { A , B } ~~ 2o <-> A =/= B ) )
2 1 pm5.32i
 |-  ( ( ( A e. _V /\ B e. _V ) /\ { A , B } ~~ 2o ) <-> ( ( A e. _V /\ B e. _V ) /\ A =/= B ) )
3 pr2cv
 |-  ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) )
4 3 pm4.71ri
 |-  ( { A , B } ~~ 2o <-> ( ( A e. _V /\ B e. _V ) /\ { A , B } ~~ 2o ) )
5 df-3an
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) <-> ( ( A e. _V /\ B e. _V ) /\ A =/= B ) )
6 2 4 5 3bitr4i
 |-  ( { A , B } ~~ 2o <-> ( A e. _V /\ B e. _V /\ A =/= B ) )