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

Theorem elrnmpt 5815
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 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2828 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐵𝐶 = 𝐵))
21rexbidv 3289 . 2 (𝑦 = 𝐶 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43rnmpt 5814 . 2 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
52, 4elab2g 3654 1 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  wrex 3134  cmpt 5132  ran crn 5543
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 5189  ax-nul 5196  ax-pr 5317
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 5053  df-opab 5115  df-mpt 5133  df-cnv 5550  df-dm 5552  df-rn 5553
This theorem is referenced by:  elrnmpt1s  5816  elrnmptdv  5820  elrnmpt2d  5821  onnseq  7977  oarec  8184  fifo  8893  infpwfien  9486  fin23lem38  9769  fin1a2lem13  9832  ac6num  9899  isercoll2  15025  iserodd  16170  gsumwspan  18011  odf1o2  18698  mplcoe5lem  20248  neitr  21788  ordtbas2  21799  ordtopn1  21802  ordtopn2  21803  pnfnei  21828  mnfnei  21829  pnrmcld  21950  2ndcomap  22066  dis2ndc  22068  ptpjopn  22220  fbasrn  22492  elfm  22555  rnelfmlem  22560  rnelfm  22561  fmfnfmlem3  22564  fmfnfmlem4  22565  fmfnfm  22566  ptcmplem2  22661  tsmsfbas  22736  ustuqtoplem  22848  utopsnneiplem  22856  utopsnnei  22858  utopreg  22861  fmucnd  22901  neipcfilu  22905  imasdsf1olem  22983  xpsdsval  22991  met1stc  23131  metustel  23160  metustsym  23165  metuel2  23175  metustbl  23176  restmetu  23180  xrtgioo  23414  minveclem3b  24035  uniioombllem3  24192  dvivth  24616  gausslemma2dlem1a  25952  elimampt  30394  acunirnmpt  30415  acunirnmpt2  30416  acunirnmpt2f  30417  fnpreimac  30427  trsp2cyc  30797  locfinreflem  31164  ordtconnlem1  31224  esumcst  31379  esumrnmpt2  31384  measdivcstALTV  31541  oms0  31612  omssubadd  31615  cvmsss2  32578  poimirlem16  35018  poimirlem19  35021  poimirlem24  35026  poimirlem27  35029  itg2addnclem2  35054  nelrnmpt  41640  suprnmpt  41721  rnmptpr  41724  elrnmptd  41731  wessf1ornlem  41736  disjrnmpt2  41740  disjf1o  41743  disjinfi  41745  choicefi  41754  rnmptlb  41805  rnmptbddlem  41806  rnmptbd2lem  41811  infnsuprnmpt  41813  elmptima  41821  supxrleubrnmpt  41969  suprleubrnmpt  41985  infrnmptle  41986  infxrunb3rnmpt  41991  supminfrnmpt  42008  infxrgelbrnmpt  42019  infrpgernmpt  42030  supminfxrrnmpt  42036  stoweidlem27  42595  stoweidlem31  42599  stoweidlem35  42603  stirlinglem5  42646  stirlinglem13  42654  fourierdlem53  42727  fourierdlem80  42754  fourierdlem93  42767  fourierdlem103  42777  fourierdlem104  42778  subsaliuncllem  42923  subsaliuncl  42924  sge0rnn0  42933  sge00  42941  fsumlesge0  42942  sge0tsms  42945  sge0cl  42946  sge0f1o  42947  sge0fsum  42952  sge0supre  42954  sge0rnbnd  42958  sge0pnffigt  42961  sge0lefi  42963  sge0ltfirp  42965  sge0resplit  42971  sge0split  42974  sge0reuz  43012  sge0reuzb  43013  hoidmvlelem2  43161  smfpimcc  43365
  Copyright terms: Public domain W3C validator