Theorem elrnmpt 5076

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

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   E.wrex 2667   e. cmpt 4226   ran crn 4838

This theorem is referenced by:  elrnmpt1s  5077  onnseq  6565  oarec  6764  fifo  7395  infpwfien  7899  fin23lem38  8185  fin1a2lem13  8248  ac6num  8315  isercoll2  12417  iserodd  13164  gsumwspan  14746  odf1o2  15162  neitr  17198  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  pnfnei  17238  mnfnei  17239  pnrmcld  17360  2ndcomap  17474  dis2ndc  17476  ptpjopn  17597  fbasrn  17869  elfm  17932  rnelfmlem  17937  rnelfm  17938  fmfnfmlem3  17941  fmfnfmlem4  17942  fmfnfm  17943  ptcmplem2  18037  tsmsfbas  18110  ustuqtoplem  18222  utopsnneiplem  18230  utopsnnei  18232  utopreg  18235  fmucnd  18275  neipcfilu  18279  imasdsf1olem  18356  xpsdsval  18364  met1stc  18504  metustelOLD  18534  metustel  18535  metustsymOLD  18544  metustsym  18545  metuel2  18562  metustblOLD  18563  metustbl  18564  restmetu  18570  xrtgioo  18790  minveclem3b  19282  uniioombllem3  19430  dvivth  19847  esumcst  24408  measdivcstOLD  24531  cvmsss2  24914  itg2addnclem2  26156  stoweidlem27  27643  stoweidlem31  27647  stoweidlem35  27651  stirlinglem5  27694  stirlinglem13  27702

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-mpt 4228  df-cnv 4845  df-dm 4847  df-rn 4848