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

Theorem elrnmpt 5909
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 2741 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐵𝐶 = 𝐵))
21rexbidv 3173 . 2 (𝑦 = 𝐶 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43rnmpt 5908 . 2 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
52, 4elab2g 3630 1 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  wrex 3071  cmpt 5186  ran crn 5632
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-mpt 5187  df-cnv 5639  df-dm 5641  df-rn 5642
This theorem is referenced by:  elrnmpt1s  5910  elrnmptd  5914  elrnmptdv  5915  elrnmpt2d  5916  onnseq  8282  oarec  8501  fifo  9326  infpwfien  9956  fin23lem38  10243  fin1a2lem13  10306  ac6num  10373  isercoll2  15513  iserodd  16667  gsumwspan  18616  odf1o2  19314  mplcoe5lem  21392  neitr  22483  ordtbas2  22494  ordtopn1  22497  ordtopn2  22498  pnfnei  22523  mnfnei  22524  pnrmcld  22645  2ndcomap  22761  dis2ndc  22763  ptpjopn  22915  fbasrn  23187  elfm  23250  rnelfmlem  23255  rnelfm  23256  fmfnfmlem3  23259  fmfnfmlem4  23260  fmfnfm  23261  ptcmplem2  23356  tsmsfbas  23431  ustuqtoplem  23543  utopsnneiplem  23551  utopsnnei  23553  utopreg  23556  fmucnd  23596  neipcfilu  23600  imasdsf1olem  23678  xpsdsval  23686  met1stc  23829  metustel  23858  metustsym  23863  metuel2  23873  metustbl  23874  restmetu  23878  xrtgioo  24121  minveclem3b  24744  uniioombllem3  24901  dvivth  25326  gausslemma2dlem1a  26665  elimampt  31381  acunirnmpt  31404  acunirnmpt2  31405  acunirnmpt2f  31406  fnpreimac  31416  trsp2cyc  31798  nsgqusf1olem2  32018  nsgqusf1olem3  32019  locfinreflem  32233  zarclsint  32265  zarcls  32267  ordtconnlem1  32317  esumcst  32474  esumrnmpt2  32479  measdivcstALTV  32636  oms0  32709  omssubadd  32712  cvmsss2  33680  poimirlem16  36032  poimirlem19  36035  poimirlem24  36040  poimirlem27  36043  itg2addnclem2  36068  nelrnmpt  43205  suprnmpt  43296  rnmptpr  43299  wessf1ornlem  43308  disjrnmpt2  43312  disjf1o  43315  disjinfi  43317  choicefi  43326  rnmptlb  43375  rnmptbddlem  43376  rnmptbd2lem  43381  infnsuprnmpt  43383  elmptima  43391  supxrleubrnmpt  43546  suprleubrnmpt  43562  infrnmptle  43563  infxrunb3rnmpt  43568  supminfrnmpt  43585  infxrgelbrnmpt  43594  infrpgernmpt  43605  supminfxrrnmpt  43611  stoweidlem27  44169  stoweidlem31  44173  stoweidlem35  44177  stirlinglem5  44220  stirlinglem13  44228  fourierdlem80  44328  fourierdlem93  44341  fourierdlem103  44351  fourierdlem104  44352  subsaliuncllem  44499  subsaliuncl  44500  sge0rnn0  44510  sge00  44518  fsumlesge0  44519  sge0tsms  44522  sge0cl  44523  sge0f1o  44524  sge0fsum  44529  sge0supre  44531  sge0rnbnd  44535  sge0pnffigt  44538  sge0lefi  44540  sge0ltfirp  44542  sge0resplit  44548  sge0split  44551  sge0reuz  44589  sge0reuzb  44590  hoidmvlelem2  44738  smfpimcc  44950
  Copyright terms: Public domain W3C validator