Theorem elrnmpt 5254

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

Hypothesis

Ref	Expression
rnmpt.1

Assertion

Ref	Expression
elrnmpt

Distinct variable group:   ,

Proof of Theorem elrnmpt

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2461	. . 3
2	1	rexbidv 2968	. 2
3		rnmpt.1	. . 3
4	3	rnmpt 5253	. 2
5	2, 4	elab2g 3248	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  E.wrex 2808  e.cmpt 4510  rancrn 5005

This theorem is referenced by:  elrnmpt1s  5255  onnseq  7034  oarec  7230  fifo  7912  infpwfien  8464  fin23lem38  8750  fin1a2lem13  8813  ac6num  8880  isercoll2  13491  iserodd  14359  gsumwspan  16014  odf1o2  16593  mplcoe5lem  18130  neitr  19681  ordtbas2  19692  ordtopn1  19695  ordtopn2  19696  pnfnei  19721  mnfnei  19722  pnrmcld  19843  2ndcomap  19959  dis2ndc  19961  ptpjopn  20113  fbasrn  20385  elfm  20448  rnelfmlem  20453  rnelfm  20454  fmfnfmlem3  20457  fmfnfmlem4  20458  fmfnfm  20459  ptcmplem2  20553  tsmsfbas  20626  ustuqtoplem  20742  utopsnneiplem  20750  utopsnnei  20752  utopreg  20755  fmucnd  20795  neipcfilu  20799  imasdsf1olem  20876  xpsdsval  20884  met1stc  21024  metustelOLD  21054  metustel  21055  metustsymOLD  21064  metustsym  21065  metuel2  21082  metustblOLD  21083  metustbl  21084  restmetu  21090  xrtgioo  21311  minveclem3b  21843  uniioombllem3  21994  dvivth  22411  locfinreflem  27843  ordtconlem1  27906  esumcst  28071  measdivcstOLD  28195  oms0  28266  cvmsss2  28719  itg2addnclem2  30067  suprnmpt  31451  stoweidlem27  31809  stoweidlem31  31813  stoweidlem35  31817  stirlinglem5  31860  stirlinglem13  31868  fourierdlem53  31942  fourierdlem80  31969  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-mpt 4512  df-cnv 5012  df-dm 5014  df-rn 5015