# 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)

Ref Expression
Hypotheses en3d.1 ${⊢}{\phi }\to {A}\in \mathrm{V}$
en3d.2 ${⊢}{\phi }\to {B}\in \mathrm{V}$
en3d.3 ${⊢}{\phi }\to \left({x}\in {A}\to {C}\in {B}\right)$
en3d.4 ${⊢}{\phi }\to \left({y}\in {B}\to {D}\in {A}\right)$
en3d.5 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({x}={D}↔{y}={C}\right)\right)$
Assertion en3d ${⊢}{\phi }\to {A}\approx {B}$

### Proof

Step Hyp Ref Expression
1 en3d.1 ${⊢}{\phi }\to {A}\in \mathrm{V}$
2 en3d.2 ${⊢}{\phi }\to {B}\in \mathrm{V}$
3 en3d.3 ${⊢}{\phi }\to \left({x}\in {A}\to {C}\in {B}\right)$
4 en3d.4 ${⊢}{\phi }\to \left({y}\in {B}\to {D}\in {A}\right)$
5 en3d.5 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({x}={D}↔{y}={C}\right)\right)$
6 eqid ${⊢}\left({x}\in {A}⟼{C}\right)=\left({x}\in {A}⟼{C}\right)$
7 3 imp ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {B}$
8 4 imp ${⊢}\left({\phi }\wedge {y}\in {B}\right)\to {D}\in {A}$
9 5 imp ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({x}={D}↔{y}={C}\right)$
10 6 7 8 9 f1o2d ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right):{A}\underset{1-1 onto}{⟶}{B}$
11 f1oen2g ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge \left({x}\in {A}⟼{C}\right):{A}\underset{1-1 onto}{⟶}{B}\right)\to {A}\approx {B}$
12 1 2 10 11 syl3anc ${⊢}{\phi }\to {A}\approx {B}$