Metamath Proof Explorer

Theorem en2d

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 12-May-2014) (Revised by AV, 4-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 en2d.1 ⊢ φ → A ∈ V
2 en2d.2 ⊢ φ → B ∈ W
3 en2d.3 ⊢ φ → x ∈ A → C ∈ X
4 en2d.4 ⊢ φ → y ∈ B → D ∈ Y
5 en2d.5 ⊢ φ → x ∈ A ∧ y = C ↔ y ∈ B ∧ x = D
6 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
7 3 imp ⊢ φ ∧ x ∈ A → C ∈ X
8 4 imp ⊢ φ ∧ y ∈ B → D ∈ Y
9 6 7 8 5 f1od ⊢ φ → x ∈ A ⟼ C : A ⟶ 1-1 onto B
10 f1oen2g ⊢ A ∈ V ∧ B ∈ W ∧ x ∈ A ⟼ C : A ⟶ 1-1 onto B → A ≈ B
11 1 2 9 10 syl3anc ⊢ φ → A ≈ B