Theorem elrnmpt 5107

Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)

Hypothesis

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

Assertion

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

Distinct variable group:   x, C

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

Proof of Theorem elrnmpt

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2449	. . 3 |- ( y = C -> ( y = B <-> C = B ) )
2	1	rexbidv 2757	. 2 |- ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
3		rnmpt.1	. . 3 |- F = ( x e. A |-> B )
4	3	rnmpt 5106	. 2 |- ran F = { y | E. x e. A y = B }
5	2, 4	elab2g 3129	1 |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   e. wcel 1756   E.wrex 2737   e. cmpt 4371   ran crn 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-mpt 4373  df-cnv 4869  df-dm 4871  df-rn 4872

This theorem is referenced by:  elrnmpt1s  5108  onnseq  6826  oarec  7022  fifo  7703  infpwfien  8253  fin23lem38  8539  fin1a2lem13  8602  ac6num  8669  isercoll2  13167  iserodd  13923  gsumwspan  15545  odf1o2  16093  mplcoe5lem  17569  neitr  18806  ordtbas2  18817  ordtopn1  18820  ordtopn2  18821  pnfnei  18846  mnfnei  18847  pnrmcld  18968  2ndcomap  19084  dis2ndc  19086  ptpjopn  19207  fbasrn  19479  elfm  19542  rnelfmlem  19547  rnelfm  19548  fmfnfmlem3  19551  fmfnfmlem4  19552  fmfnfm  19553  ptcmplem2  19647  tsmsfbas  19720  ustuqtoplem  19836  utopsnneiplem  19844  utopsnnei  19846  utopreg  19849  fmucnd  19889  neipcfilu  19893  imasdsf1olem  19970  xpsdsval  19978  met1stc  20118  metustelOLD  20148  metustel  20149  metustsymOLD  20158  metustsym  20159  metuel2  20176  metustblOLD  20177  metustbl  20178  restmetu  20184  xrtgioo  20405  minveclem3b  20937  uniioombllem3  21087  dvivth  21504  ordtconlem1  26376  esumcst  26536  measdivcstOLD  26660  oms0  26732  cvmsss2  27185  itg2addnclem2  28470  stoweidlem27  29848  stoweidlem31  29852  stoweidlem35  29856  stirlinglem5  29899  stirlinglem13  29907