Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
enpr2d
Metamath Proof Explorer
Description: A pair with distinct elements is equinumerous to ordinal two.
(Contributed by Rohan Ridenour , 3-Aug-2023) Avoid ax-un . (Revised by BTernaryTau , 23-Dec-2024)
Ref
Expression
Hypotheses
enpr2d.1
⊢ φ → A ∈ C
enpr2d.2
⊢ φ → B ∈ D
enpr2d.3
⊢ φ → ¬ A = B
Assertion
enpr2d
⊢ φ → A B ≈ 2 𝑜
Proof
Step
Hyp
Ref
Expression
1
enpr2d.1
⊢ φ → A ∈ C
2
enpr2d.2
⊢ φ → B ∈ D
3
enpr2d.3
⊢ φ → ¬ A = B
4
0ex
⊢ ∅ ∈ V
5
4
a1i
⊢ φ → ∅ ∈ V
6
1oex
⊢ 1 𝑜 ∈ V
7
6
a1i
⊢ φ → 1 𝑜 ∈ V
8
3
neqned
⊢ φ → A ≠ B
9
1n0
⊢ 1 𝑜 ≠ ∅
10
9
necomi
⊢ ∅ ≠ 1 𝑜
11
10
a1i
⊢ φ → ∅ ≠ 1 𝑜
12
1 2 5 7 8 11
en2prd
⊢ φ → A B ≈ ∅ 1 𝑜
13
df2o3
⊢ 2 𝑜 = ∅ 1 𝑜
14
12 13
breqtrrdi
⊢ φ → A B ≈ 2 𝑜