Description: An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d . (Contributed by FL, 17-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | enpr2 | |- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ne | |- ( A =/= B <-> -. A = B ) |
|
| 2 | simp1 | |- ( ( A e. C /\ B e. D /\ -. A = B ) -> A e. C ) |
|
| 3 | simp2 | |- ( ( A e. C /\ B e. D /\ -. A = B ) -> B e. D ) |
|
| 4 | simp3 | |- ( ( A e. C /\ B e. D /\ -. A = B ) -> -. A = B ) |
|
| 5 | 2 3 4 | enpr2d | |- ( ( A e. C /\ B e. D /\ -. A = B ) -> { A , B } ~~ 2o ) |
| 6 | 1 5 | syl3an3b | |- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o ) |