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

Theorem rnmpt 5815
 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 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥,𝑦)

Proof of Theorem rnmpt
StepHypRef Expression
1 rnopab 5814 . 2 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
2 rnmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐵)
3 df-mpt 5134 . . . 4 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
42, 3eqtri 2847 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
54rneqi 5795 . 2 ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
6 df-rex 3139 . . 3 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥𝐴𝑦 = 𝐵))
76abbii 2889 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
81, 5, 73eqtr4i 2857 1 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2115  {cab 2802  ∃wrex 3134  {copab 5115   ↦ cmpt 5133  ran crn 5544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pr 5318 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rex 3139  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-br 5054  df-opab 5116  df-mpt 5134  df-cnv 5551  df-dm 5553  df-rn 5554 This theorem is referenced by:  elrnmpt  5816  elrnmpt1  5818  elrnmptg  5819  dfiun3g  5824  dfiin3g  5825  fnrnfv  6718  fmpt  6867  fnasrn  6900  fliftf  7063  abrexexg  7659  fo1st  7706  fo2nd  7707  fsplitfpar  7812  qliftf  8383  abrexfi  8823  iinfi  8880  tz9.12lem1  9215  infmap2  9640  cfslb2n  9690  fin23lem29  9763  fin23lem30  9764  fin1a2lem11  9832  ac6num  9901  rankcf  10199  tskuni  10205  negfi  11588  4sqlem11  16291  4sqlem12  16292  vdwapval  16309  vdwlem6  16322  quslem  16818  smndex2dnrinv  18082  conjnmzb  18395  pmtrprfvalrn  18618  sylow1lem2  18726  sylow3lem1  18754  sylow3lem2  18755  ablsimpgfind  19234  ellspd  20500  rnascl  20586  iinopn  21516  restco  21778  pnrmopn  21957  cncmp  22006  discmp  22012  comppfsc  22146  alexsublem  22658  ptcmplem3  22668  snclseqg  22730  prdsxmetlem  22984  prdsbl  23107  xrhmeo  23560  pi1xfrf  23667  pi1cof  23673  iunmbl  24166  voliun  24167  itg1addlem4  24312  i1fmulc  24316  mbfi1fseqlem4  24331  itg2monolem1  24363  aannenlem2  24934  2lgslem1b  25985  mptelee  26698  disjrnmpt  30354  ofrn2  30406  abrexct  30473  abrexctf  30475  esumc  31395  esumrnmpt  31396  carsgclctunlem3  31663  eulerpartlemt  31714  bdayfo  33267  nosupno  33288  fobigcup  33446  ptrest  35028  areacirclem2  35118  istotbnd3  35181  sstotbnd  35185  dfqs2  39377  rnasclg  39386  rmxypairf1o  39796  hbtlem6  40017  elrnmptf  41759  fnrnafv  43671  fundcmpsurinjlem1  43868  imasetpreimafvbijlemfo  43875  fargshiftfo  43912
 Copyright terms: Public domain W3C validator