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

Theorem rnmpt 5522
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 5521 . 2 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
2 rnmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐵)
3 df-mpt 4878 . . . 4 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
42, 3eqtri 2778 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
54rneqi 5503 . 2 ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
6 df-rex 3052 . . 3 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥𝐴𝑦 = 𝐵))
76abbii 2873 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
81, 5, 73eqtr4i 2788 1 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1628  wex 1849  wcel 2135  {cab 2742  wrex 3047  {copab 4860  cmpt 4877  ran crn 5263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4801  df-opab 4861  df-mpt 4878  df-cnv 5270  df-dm 5272  df-rn 5273
This theorem is referenced by:  elrnmpt  5523  elrnmpt1  5525  elrnmptg  5526  dfiun3g  5529  dfiin3g  5530  fnrnfv  6400  fmpt  6540  fnasrn  6570  fliftf  6724  abrexexg  7301  abrexexOLD  7303  fo1st  7349  fo2nd  7350  qliftf  7998  abrexfi  8427  iinfi  8484  tz9.12lem1  8819  infmap2  9228  cfslb2n  9278  fin23lem29  9351  fin23lem30  9352  fin1a2lem11  9420  ac6num  9489  rankcf  9787  tskuni  9793  negfi  11159  4sqlem11  15857  4sqlem12  15858  vdwapval  15875  vdwlem6  15888  quslem  16401  conjnmzb  17892  pmtrprfvalrn  18104  sylow1lem2  18210  sylow3lem1  18238  sylow3lem2  18239  rnascl  19541  ellspd  20339  iinopn  20905  restco  21166  pnrmopn  21345  cncmp  21393  discmp  21399  comppfsc  21533  alexsublem  22045  ptcmplem3  22055  snclseqg  22116  prdsxmetlem  22370  prdsbl  22493  xrhmeo  22942  pi1xfrf  23049  pi1cof  23055  iunmbl  23517  voliun  23518  itg1addlem4  23661  i1fmulc  23665  mbfi1fseqlem4  23680  itg2monolem1  23712  aannenlem2  24279  2lgslem1b  25312  mptelee  25970  disjrnmpt  29701  ofrn2  29747  abrexct  29799  abrexctf  29801  esumc  30418  esumrnmpt  30419  carsgclctunlem3  30687  eulerpartlemt  30738  bdayfo  32130  nosupno  32151  fobigcup  32309  ptrest  33717  areacirclem2  33810  istotbnd3  33879  sstotbnd  33883  rmxypairf1o  37974  hbtlem6  38197  elrnmptf  39862  fnrnafv  41744  fargshiftfo  41884
  Copyright terms: Public domain W3C validator