Theorem elrnmpt 5081

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 2455	. . 3 |- ( y = C -> ( y = B <-> C = B ) )
2	1	rexbidv 2901	. 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 5080	. 2 |- ran F = { y | E. x e. A y = B }
5	2, 4	elab2g 3187	1 |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   e. wcel 1887   E.wrex 2738   |-> cmpt 4461   ran crn 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-mpt 4463  df-cnv 4842  df-dm 4844  df-rn 4845

This theorem is referenced by:  elrnmpt1s  5082  onnseq  7063  oarec  7263  fifo  7946  infpwfien  8493  fin23lem38  8779  fin1a2lem13  8842  ac6num  8909  isercoll2  13732  iserodd  14785  gsumwspan  16630  odf1o2  17222  mplcoe5lem  18691  neitr  20196  ordtbas2  20207  ordtopn1  20210  ordtopn2  20211  pnfnei  20236  mnfnei  20237  pnrmcld  20358  2ndcomap  20473  dis2ndc  20475  ptpjopn  20627  fbasrn  20899  elfm  20962  rnelfmlem  20967  rnelfm  20968  fmfnfmlem3  20971  fmfnfmlem4  20972  fmfnfm  20973  ptcmplem2  21068  tsmsfbas  21142  ustuqtoplem  21254  utopsnneiplem  21262  utopsnnei  21264  utopreg  21267  fmucnd  21307  neipcfilu  21311  imasdsf1olem  21388  xpsdsval  21396  met1stc  21536  metustel  21565  metustsym  21570  metuel2  21580  metustbl  21581  restmetu  21585  xrtgioo  21824  minveclem3b  22370  minveclem3bOLD  22382  uniioombllem3  22543  dvivth  22962  acunirnmpt  28261  acunirnmpt2  28262  acunirnmpt2f  28263  locfinreflem  28667  ordtconlem1  28730  esumcst  28884  esumrnmpt2  28889  measdivcstOLD  29046  oms0  29125  omssubadd  29128  oms0OLD  29129  omssubaddOLD  29132  cvmsss2  29997  poimirlem16  31956  poimirlem19  31959  poimirlem24  31964  poimirlem27  31967  itg2addnclem2  31994  suprnmpt  37439  rnmptpr  37444  elrnmptd  37453  rnmptssrn  37456  wessf1ornlem  37459  disjrnmpt2  37463  disjf1o  37466  disjinfi  37468  choicefi  37481  stoweidlem27  37887  stoweidlem31  37892  stoweidlem35  37896  stirlinglem5  37940  stirlinglem13  37948  fourierdlem53  38023  fourierdlem80  38050  fourierdlem93  38063  fourierdlem103  38073  fourierdlem104  38074  sge0rnn0  38210  sge00  38218  fsumlesge0  38219  sge0tsms  38222  sge0cl  38223  sge0f1o  38224  sge0fsum  38229  sge0supre  38231  sge0rnbnd  38235  sge0pnffigt  38238  sge0lefi  38240  sge0ltfirp  38242  sge0resplit  38248  sge0split  38251  hoidmvlelem2  38418