MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnmpt Unicode version

Theorem rnmpt 5253
Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
rnmpt.1
Assertion
Ref Expression
rnmpt
Distinct variable groups:   ,   ,   ,

Proof of Theorem rnmpt
StepHypRef Expression
1 rnopab 5252 . 2
2 rnmpt.1 . . . 4
3 df-mpt 4512 . . . 4
42, 3eqtri 2486 . . 3
54rneqi 5234 . 2
6 df-rex 2813 . . 3
76abbii 2591 . 2
81, 5, 73eqtr4i 2496 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442  E.wrex 2808  {copab 4509  e.cmpt 4510  rancrn 5005
This theorem is referenced by:  elrnmpt  5254  elrnmpt1  5256  elrnmptg  5257  dfiun3g  5260  dfiin3g  5261  fnrnfv  5919  fmpt  6052  fnasrn  6077  fliftf  6213  abrexex  6774  abrexexg  6775  fo1st  6820  fo2nd  6821  qliftf  7418  abrexfi  7840  iinfi  7897  tz9.12lem1  8226  infmap2  8619  cfslb2n  8669  fin23lem29  8742  fin23lem30  8743  fin1a2lem11  8811  ac6num  8880  rankcf  9176  tskuni  9182  4sqlem11  14473  4sqlem12  14474  vdwapval  14491  vdwlem6  14504  quslem  14940  conjnmzb  16301  pmtrprfvalrn  16513  sylow1lem2  16619  sylow3lem1  16647  sylow3lem2  16648  rnascl  17992  ellspd  18836  ellspdOLD  18837  iinopn  19411  restco  19665  pnrmopn  19844  cncmp  19892  discmp  19898  comppfsc  20033  alexsublem  20544  ptcmplem3  20554  snclseqg  20614  prdsxmetlem  20871  prdsbl  20994  xrhmeo  21446  pi1xfrf  21553  pi1cof  21559  iunmbl  21963  voliun  21964  itg1addlem4  22106  i1fmulc  22110  mbfi1fseqlem4  22125  itg2monolem1  22157  aannenlem2  22725  mptelee  24198  nbgraf1olem5  24445  fargshiftfo  24638  efghgrpOLD  25375  circgrpOLD  25376  ofrn2  27480  abrexct  27543  abrexctf  27545  esumc  28062  eulerpartlemt  28310  bdayfo  29435  fobigcup  29550  ptrest  30048  areacirclem2  30108  istotbnd3  30267  sstotbnd  30271  rmxypairf1o  30847  hbtlem6  31078  fnrnafv  32247
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
  Copyright terms: Public domain W3C validator