Metamath Proof Explorer


Theorem f1dom

Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998)

Ref Expression
Hypothesis f1dom.1 𝐵 ∈ V
Assertion f1dom ( 𝐹 : 𝐴1-1𝐵𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 f1dom.1 𝐵 ∈ V
2 f1domg ( 𝐵 ∈ V → ( 𝐹 : 𝐴1-1𝐵𝐴𝐵 ) )
3 1 2 ax-mp ( 𝐹 : 𝐴1-1𝐵𝐴𝐵 )