Metamath Proof Explorer

Theorem elpmrn

Description: The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion elpmrn 
|- ( F e. ( A ^pm B ) -> ran F C_ A )

Proof

Step Hyp Ref Expression
1 elpmi 
 |-  ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )
2 1 simpld 
 |-  ( F e. ( A ^pm B ) -> F : dom F --> A )
3 2 frnd 
 |-  ( F e. ( A ^pm B ) -> ran F C_ A )