Metamath Proof Explorer

Theorem en2i

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004)

Ref Expression
Hypotheses en2i.1 ⊢ A ∈ V
en2i.2 ⊢ B ∈ V
en2i.3 ⊢ x ∈ A → C ∈ V
en2i.4 ⊢ y ∈ B → D ∈ V
en2i.5 ⊢ x ∈ A ∧ y = C ↔ y ∈ B ∧ x = D
Assertion en2i ⊢ A ≈ B

Proof

Step Hyp Ref Expression
1 en2i.1 ⊢ A ∈ V
2 en2i.2 ⊢ B ∈ V
3 en2i.3 ⊢ x ∈ A → C ∈ V
4 en2i.4 ⊢ y ∈ B → D ∈ V
5 en2i.5 ⊢ x ∈ A ∧ y = C ↔ y ∈ B ∧ x = D
6 1 a1i ⊢ ⊤ → A ∈ V
7 2 a1i ⊢ ⊤ → B ∈ V
8 3 a1i ⊢ ⊤ → x ∈ A → C ∈ V
9 4 a1i ⊢ ⊤ → y ∈ B → D ∈ V
10 5 a1i ⊢ ⊤ → x ∈ A ∧ y = C ↔ y ∈ B ∧ x = D
11 6 7 8 9 10 en2d ⊢ ⊤ → A ≈ B
12 11 mptru ⊢ A ≈ B