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