This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Equinumerosity f1imaen
Description: If a function is one-to-one, then the image of a subset of its domain
under it 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 → 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )