Metamath Proof Explorer


Theorem elrnmpt1d

Description: Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses elrnmpt1d.1
|- F = ( x e. A |-> B )
elrnmpt1d.2
|- ( ph -> x e. A )
elrnmpt1d.3
|- ( ph -> B e. V )
Assertion elrnmpt1d
|- ( ph -> B e. ran F )

Proof

Step Hyp Ref Expression
1 elrnmpt1d.1
 |-  F = ( x e. A |-> B )
2 elrnmpt1d.2
 |-  ( ph -> x e. A )
3 elrnmpt1d.3
 |-  ( ph -> B e. V )
4 1 elrnmpt1
 |-  ( ( x e. A /\ B e. V ) -> B e. ran F )
5 2 3 4 syl2anc
 |-  ( ph -> B e. ran F )