Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | f1domg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1f | |
|
2 | f1dmex | |
|
3 | fex | |
|
4 | 1 2 3 | syl2an2r | |
5 | 4 | expcom | |
6 | f1eq1 | |
|
7 | 6 | spcegv | |
8 | 5 7 | syli | |
9 | brdomg | |
|
10 | 8 9 | sylibrd | |