Metamath Proof Explorer


Theorem f1oen3g

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 NM, 13-Jan-2007) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion f1oen3g F V F : A 1-1 onto B A B

Proof

Step Hyp Ref Expression
1 f1oeq1 f = F f : A 1-1 onto B F : A 1-1 onto B
2 1 spcegv F V F : A 1-1 onto B f f : A 1-1 onto B
3 2 imp F V F : A 1-1 onto B f f : A 1-1 onto B
4 bren A B f f : A 1-1 onto B
5 3 4 sylibr F V F : A 1-1 onto B A B