Metamath Proof Explorer

Theorem enpr2

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 ∈ C ∧ B ∈ D ∧ A ≠ B → A B ≈ 2 𝑜

Proof

Step Hyp Ref Expression
1 df-ne ⊢ A ≠ B ↔ ¬ A = B
2 simp1 ⊢ A ∈ C ∧ B ∈ D ∧ ¬ A = B → A ∈ C
3 simp2 ⊢ A ∈ C ∧ B ∈ D ∧ ¬ A = B → B ∈ D
4 simp3 ⊢ A ∈ C ∧ B ∈ D ∧ ¬ A = B → ¬ A = B
5 2 3 4 enpr2d ⊢ A ∈ C ∧ B ∈ D ∧ ¬ A = B → A B ≈ 2 𝑜
6 1 5 syl3an3b ⊢ A ∈ C ∧ B ∈ D ∧ A ≠ B → A B ≈ 2 𝑜