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 e. V /\ F : A -1-1-onto-> B ) -> A ~~ B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq1 | |- ( f = F -> ( f : A -1-1-onto-> B <-> F : A -1-1-onto-> B ) ) |
|
2 | 1 | spcegv | |- ( F e. V -> ( F : A -1-1-onto-> B -> E. f f : A -1-1-onto-> B ) ) |
3 | 2 | imp | |- ( ( F e. V /\ F : A -1-1-onto-> B ) -> E. f f : A -1-1-onto-> B ) |
4 | bren | |- ( A ~~ B <-> E. f f : A -1-1-onto-> B ) |
|
5 | 3 4 | sylibr | |- ( ( F e. V /\ F : A -1-1-onto-> B ) -> A ~~ B ) |