This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en3i

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

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

Proof

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