Metamath Proof Explorer


Theorem f1domg

Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004)

Ref Expression
Assertion f1domg BCF:A1-1BAB

Proof

Step Hyp Ref Expression
1 f1f F:A1-1BF:AB
2 f1dmex F:A1-1BBCAV
3 fex F:ABAVFV
4 1 2 3 syl2an2r F:A1-1BBCFV
5 4 expcom BCF:A1-1BFV
6 f1eq1 f=Ff:A1-1BF:A1-1B
7 6 spcegv FVF:A1-1Bff:A1-1B
8 5 7 syli BCF:A1-1Bff:A1-1B
9 brdomg BCABff:A1-1B
10 8 9 sylibrd BCF:A1-1BAB