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

Theorem rnmpt 5540
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 5539 . 2 ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
2 rnmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐵)
3 df-mpt 4889 . . . 4 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
42, 3eqtri 2787 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
54rneqi 5520 . 2 ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
6 df-rex 3061 . . 3 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥𝐴𝑦 = 𝐵))
76abbii 2882 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 = 𝐵)}
81, 5, 73eqtr4i 2797 1 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wrex 3056  {copab 4871  cmpt 4888  ran crn 5278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810  df-opab 4872  df-mpt 4889  df-cnv 5285  df-dm 5287  df-rn 5288
This theorem is referenced by:  elrnmpt  5541  elrnmpt1  5543  elrnmptg  5544  dfiun3g  5547  dfiin3g  5548  fnrnfv  6431  fmpt  6570  fnasrn  6602  fliftf  6757  abrexexg  7338  abrexexOLD  7340  fo1st  7386  fo2nd  7387  qliftf  8038  abrexfi  8473  iinfi  8530  tz9.12lem1  8865  infmap2  9293  cfslb2n  9343  fin23lem29  9416  fin23lem30  9417  fin1a2lem11  9485  ac6num  9554  rankcf  9852  tskuni  9858  negfi  11225  4sqlem11  15940  4sqlem12  15941  vdwapval  15958  vdwlem6  15971  quslem  16471  conjnmzb  17961  pmtrprfvalrn  18173  sylow1lem2  18280  sylow3lem1  18308  sylow3lem2  18309  rnascl  19617  ellspd  20417  iinopn  20986  restco  21248  pnrmopn  21427  cncmp  21475  discmp  21481  comppfsc  21615  alexsublem  22127  ptcmplem3  22137  snclseqg  22198  prdsxmetlem  22452  prdsbl  22575  xrhmeo  23024  pi1xfrf  23131  pi1cof  23137  iunmbl  23611  voliun  23612  itg1addlem4  23757  i1fmulc  23761  mbfi1fseqlem4  23776  itg2monolem1  23808  aannenlem2  24375  2lgslem1b  25408  mptelee  26066  disjrnmpt  29781  ofrn2  29827  abrexct  29878  abrexctf  29880  esumc  30495  esumrnmpt  30496  carsgclctunlem3  30764  eulerpartlemt  30815  bdayfo  32204  nosupno  32225  fobigcup  32383  ptrest  33764  areacirclem2  33856  istotbnd3  33924  sstotbnd  33928  rmxypairf1o  38085  hbtlem6  38308  elrnmptf  39946  fnrnafv  41842  fargshiftfo  42044
  Copyright terms: Public domain W3C validator