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 |
⊢ 𝐶 ∈ V |
|
Assertion |
f1imaen |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
f1imaen.1 |
⊢ 𝐶 ∈ V |
2 |
|
f1imaeng |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) |
3 |
1 2
|
mp3an3 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) |