Theorem elrnmpt1d

Description: Elementhood in an image set. Deducion version of elrnmpt1 . (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 )