Metamath Proof Explorer


Theorem elrnmpti

Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses rnmpt.1 F=xAB
elrnmpti.2 BV
Assertion elrnmpti CranFxAC=B

Proof

Step Hyp Ref Expression
1 rnmpt.1 F=xAB
2 elrnmpti.2 BV
3 2 rgenw xABV
4 1 elrnmptg xABVCranFxAC=B
5 3 4 ax-mp CranFxAC=B