Theorem elrnmpt2d

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

	Ref	Expression
Hypotheses	elrnmpt2d.1	|- F = ( x e. A |-> B )
	elrnmpt2d.2	|- ( ph -> C e. ran F )
Assertion	elrnmpt2d	|- ( ph -> E. x e. A C = B )

Proof

Step	Hyp	Ref	Expression
1		elrnmpt2d.1	|- F = ( x e. A |-> B )
2		elrnmpt2d.2	|- ( ph -> C e. ran F )
3	1	elrnmpt	|- ( C e. ran F -> ( C e. ran F <-> E. x e. A C = B ) )
4	3	ibi	|- ( C e. ran F -> E. x e. A C = B )
5	2 4	syl	|- ( ph -> E. x e. A C = B )