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

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

### Proof

Step Hyp Ref Expression
1 en2d.1 ${⊢}{\phi }\to {A}\in \mathrm{V}$
2 en2d.2 ${⊢}{\phi }\to {B}\in \mathrm{V}$
3 en2d.3 ${⊢}{\phi }\to \left({x}\in {A}\to {C}\in \mathrm{V}\right)$
4 en2d.4 ${⊢}{\phi }\to \left({y}\in {B}\to {D}\in \mathrm{V}\right)$
5 en2d.5 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}={C}\right)↔\left({y}\in {B}\wedge {x}={D}\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 \mathrm{V}$
8 4 imp ${⊢}\left({\phi }\wedge {y}\in {B}\right)\to {D}\in \mathrm{V}$
9 6 7 8 5 f1od ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right):{A}\underset{1-1 onto}{⟶}{B}$
10 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}$
11 1 2 9 10 syl3anc ${⊢}{\phi }\to {A}\approx {B}$