Metamath Proof Explorer

Theorem en3d

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 en3d.1 ⊢ φ → A ∈ V
en3d.2 ⊢ φ → B ∈ W
en3d.3 ⊢ φ → x ∈ A → C ∈ B
en3d.4 ⊢ φ → y ∈ B → D ∈ A
en3d.5 ⊢ φ → x ∈ A ∧ y ∈ B → x = D ↔ y = C
Assertion en3d ⊢ φ → A ≈ B

Proof

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