Theorem rr-elrnmpt3d

Description: Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	rr-elrnmpt3d.1	$$⊢F=\left(x\in A⟼B\right)$$
	rr-elrnmpt3d.2	$$⊢\phi \to C\in A$$
	rr-elrnmpt3d.3	$$⊢\phi \to D\in V$$
	rr-elrnmpt3d.4	$$⊢\left(\phi \wedge x=C\right)\to B=D$$
Assertion	rr-elrnmpt3d	$$⊢\phi \to D\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		rr-elrnmpt3d.1	$$⊢F=\left(x\in A⟼B\right)$$
2		rr-elrnmpt3d.2	$$⊢\phi \to C\in A$$
3		rr-elrnmpt3d.3	$$⊢\phi \to D\in V$$
4		rr-elrnmpt3d.4	$$⊢\left(\phi \wedge x=C\right)\to B=D$$
5	4	eqcomd	$$⊢\left(\phi \wedge x=C\right)\to D=B$$
6	1 2 3 5	elrnmptdv	$$⊢\phi \to D\in \mathrm{ran}F$$