Theorem elrnmpti 5084

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

Hypotheses

Ref	Expression
rnmpt.1	|- F = ( x e. A |-> B )
elrnmpti.2	|- B e. _V

Assertion

Ref	Expression
elrnmpti	|- ( C e. ran F <-> E. x e. A C = B )

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)   F( x)

Proof of Theorem elrnmpti

Step	Hyp	Ref	Expression
1		elrnmpti.2	. . 3 |- B e. _V
2	1	rgenw 2748	. 2 |- A. x e. A B e. _V
3		rnmpt.1	. . 3 |- F = ( x e. A |-> B )
4	3	elrnmptg 5083	. 2 |- ( A. x e. A B e. _V -> ( C e. ran F <-> E. x e. A C = B ) )
5	2, 4	ax-mp 5	1 |- ( C e. ran F <-> E. x e. A C = B )

Syntax hints:   <-> wb 188   = wceq 1443   e. wcel 1886   A.wral 2736   E.wrex 2737   _Vcvv 3044   |-> cmpt 4460   ran crn 4834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-mpt 4462  df-cnv 4841  df-dm 4843  df-rn 4844

This theorem is referenced by:  fliftel  6200  oarec  7260  unfilem1  7832  pwfilem  7865  elrest  15319  psgneldm2  17138  psgnfitr  17151  iscyggen2  17509  iscyg3  17514  cycsubgcyg  17528  eldprd  17629  leordtval2  20221  iocpnfordt  20224  icomnfordt  20225  lecldbas  20228  tsmsxplem1  21160  minveclem2  22361  minveclem2OLD  22373  lhop2  22960  taylthlem2  23322  fsumvma  24134  dchrptlem2  24186  2sqlem1  24284  dchrisum0fno1  24342  minvecolem2  26510  minvecolem2OLD  26520  gsumesum  28873  esumlub  28874  esumcst  28877  esumpcvgval  28892  esumgect  28904  esum2d  28907  sigapildsys  28977  sxbrsigalem2  29101  omssubaddlem  29120  omssubadd  29121  omssubaddlemOLD  29124  omssubaddOLD  29125  eulerpartgbij  29198  bnj1366  29634  msubco  30162  msubvrs  30191  fin2so  31925  poimirlem17  31950  poimirlem20  31953  cntotbnd  32121  islsat  32551