Metamath Proof Explorer
Description: A one-to-one function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30-Sep-2004)
|
|
Ref |
Expression |
|
Hypothesis |
f1imaen.1 |
|
|
Assertion |
f1imaen |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
f1imaen.1 |
|
2 |
|
f1imaeng |
|
3 |
1 2
|
mp3an3 |
|