Metamath Proof Explorer


Theorem rnmptss

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017)

Ref Expression
Hypothesis rnmptss.1
|- F = ( x e. A |-> B )
Assertion rnmptss
|- ( A. x e. A B e. C -> ran F C_ C )

Proof

Step Hyp Ref Expression
1 rnmptss.1
 |-  F = ( x e. A |-> B )
2 1 fmpt
 |-  ( A. x e. A B e. C <-> F : A --> C )
3 frn
 |-  ( F : A --> C -> ran F C_ C )
4 2 3 sylbi
 |-  ( A. x e. A B e. C -> ran F C_ C )