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 φ A V
en2d.2 φ B V
en2d.3 φ x A C V
en2d.4 φ y B D V
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 V
3 en2d.3 φ x A C V
4 en2d.4 φ y B D V
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 V
8 4 imp φ y B D V
9 6 7 8 5 f1od φ x A C : A 1-1 onto B
10 f1oen2g A V B V x A C : A 1-1 onto B A B
11 1 2 9 10 syl3anc φ A B