Metamath Proof Explorer


Theorem f1oen2g

Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion f1oen2g AVBWF:A1-1 ontoBAB

Proof

Step Hyp Ref Expression
1 f1of F:A1-1 ontoBF:AB
2 fex2 F:ABAVBWFV
3 1 2 syl3an1 F:A1-1 ontoBAVBWFV
4 3 3coml AVBWF:A1-1 ontoBFV
5 simp3 AVBWF:A1-1 ontoBF:A1-1 ontoB
6 f1oen3g FVF:A1-1 ontoBAB
7 4 5 6 syl2anc AVBWF:A1-1 ontoBAB