Theorem elrnmpt 5087

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   e. wcel 1904   E.wrex 2757   |-> cmpt 4454   ran crn 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-mpt 4456  df-cnv 4847  df-dm 4849  df-rn 4850

This theorem is referenced by:  elrnmpt1s  5088  onnseq  7081  oarec  7281  fifo  7964  infpwfien  8511  fin23lem38  8797  fin1a2lem13  8860  ac6num  8927  isercoll2  13809  iserodd  14864  gsumwspan  16708  odf1o2  17300  mplcoe5lem  18768  neitr  20273  ordtbas2  20284  ordtopn1  20287  ordtopn2  20288  pnfnei  20313  mnfnei  20314  pnrmcld  20435  2ndcomap  20550  dis2ndc  20552  ptpjopn  20704  fbasrn  20977  elfm  21040  rnelfmlem  21045  rnelfm  21046  fmfnfmlem3  21049  fmfnfmlem4  21050  fmfnfm  21051  ptcmplem2  21146  tsmsfbas  21220  ustuqtoplem  21332  utopsnneiplem  21340  utopsnnei  21342  utopreg  21345  fmucnd  21385  neipcfilu  21389  imasdsf1olem  21466  xpsdsval  21474  met1stc  21614  metustel  21643  metustsym  21648  metuel2  21658  metustbl  21659  restmetu  21663  xrtgioo  21902  minveclem3b  22448  minveclem3bOLD  22460  uniioombllem3  22622  dvivth  23041  acunirnmpt  28336  acunirnmpt2  28337  acunirnmpt2f  28338  locfinreflem  28741  ordtconlem1  28804  esumcst  28958  esumrnmpt2  28963  measdivcstOLD  29120  oms0  29198  omssubadd  29201  oms0OLD  29202  omssubaddOLD  29205  cvmsss2  30069  poimirlem16  32020  poimirlem19  32023  poimirlem24  32028  poimirlem27  32031  itg2addnclem2  32058  nelrnmpt  37492  suprnmpt  37512  rnmptpr  37515  elrnmptd  37524  rnmptssrn  37527  wessf1ornlem  37530  disjrnmpt2  37534  disjf1o  37537  disjinfi  37539  choicefi  37552  stoweidlem27  37999  stoweidlem31  38004  stoweidlem35  38008  stirlinglem5  38052  stirlinglem13  38060  fourierdlem53  38135  fourierdlem80  38162  fourierdlem93  38175  fourierdlem103  38185  fourierdlem104  38186  sge0rnn0  38324  sge00  38332  fsumlesge0  38333  sge0tsms  38336  sge0cl  38337  sge0f1o  38338  sge0fsum  38343  sge0supre  38345  sge0rnbnd  38349  sge0pnffigt  38352  sge0lefi  38354  sge0ltfirp  38356  sge0resplit  38362  sge0split  38365  hoidmvlelem2  38536