# Metamath Proof Explorer

## Theorem f1imaen2g

Description: A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen does not need ax-reg .) (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion f1imaen2g ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {F}\left[{C}\right]\approx {C}$

### Proof

Step Hyp Ref Expression
1 simprr ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {C}\in {V}$
2 simplr ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {B}\in {V}$
3 f1f ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}:{A}⟶{B}$
4 fimass ${⊢}{F}:{A}⟶{B}\to {F}\left[{C}\right]\subseteq {B}$
5 3 4 syl ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}\left[{C}\right]\subseteq {B}$
6 5 ad2antrr ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {F}\left[{C}\right]\subseteq {B}$
7 2 6 ssexd ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {F}\left[{C}\right]\in \mathrm{V}$
8 f1ores ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{1-1 onto}{⟶}{F}\left[{C}\right]$
9 8 ad2ant2r ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{1-1 onto}{⟶}{F}\left[{C}\right]$
10 f1oen2g ${⊢}\left({C}\in {V}\wedge {F}\left[{C}\right]\in \mathrm{V}\wedge \left({{F}↾}_{{C}}\right):{C}\underset{1-1 onto}{⟶}{F}\left[{C}\right]\right)\to {C}\approx {F}\left[{C}\right]$
11 1 7 9 10 syl3anc ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {C}\approx {F}\left[{C}\right]$
12 11 ensymd ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in {V}\right)\wedge \left({C}\subseteq {A}\wedge {C}\in {V}\right)\right)\to {F}\left[{C}\right]\approx {C}$