Metamath Proof Explorer


Theorem fodom

Description: An onto function implies dominance of domain over range. (Contributed by NM, 23-Jul-2004)

Ref Expression
Hypothesis fodom.1 𝐴 ∈ V
Assertion fodom ( 𝐹 : 𝐴onto𝐵𝐵𝐴 )

Proof

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