Theorem elrnmptdv

Description: Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	elrnmptdv.1	|- F = ( x e. A |-> B )
	elrnmptdv.2	|- ( ph -> C e. A )
	elrnmptdv.3	|- ( ph -> D e. V )
	elrnmptdv.4	|- ( ( ph /\ x = C ) -> D = B )
Assertion	elrnmptdv	|- ( ph -> D e. ran F )

Proof

Step	Hyp	Ref	Expression
1		elrnmptdv.1	|- F = ( x e. A |-> B )
2		elrnmptdv.2	|- ( ph -> C e. A )
3		elrnmptdv.3	|- ( ph -> D e. V )
4		elrnmptdv.4	|- ( ( ph /\ x = C ) -> D = B )
5	4 2	rspcime	|- ( ph -> E. x e. A D = B )
6	1	elrnmpt	|- ( D e. V -> ( D e. ran F <-> E. x e. A D = B ) )
7	3 6	syl	|- ( ph -> ( D e. ran F <-> E. x e. A D = B ) )
8	5 7	mpbird	|- ( ph -> D e. ran F )