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

Theorem elrnmpt 5821
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 2822 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐵𝐶 = 𝐵))
21rexbidv 3294 . 2 (𝑦 = 𝐶 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43rnmpt 5820 . 2 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
52, 4elab2g 3665 1 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wrex 3136  cmpt 5137  ran crn 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-mpt 5138  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  elrnmpt1s  5822  elrnmptdv  5826  elrnmpt2d  5827  onnseq  7970  oarec  8177  fifo  8884  infpwfien  9476  fin23lem38  9759  fin1a2lem13  9822  ac6num  9889  isercoll2  15013  iserodd  16160  gsumwspan  17999  odf1o2  18627  mplcoe5lem  20176  neitr  21716  ordtbas2  21727  ordtopn1  21730  ordtopn2  21731  pnfnei  21756  mnfnei  21757  pnrmcld  21878  2ndcomap  21994  dis2ndc  21996  ptpjopn  22148  fbasrn  22420  elfm  22483  rnelfmlem  22488  rnelfm  22489  fmfnfmlem3  22492  fmfnfmlem4  22493  fmfnfm  22494  ptcmplem2  22589  tsmsfbas  22663  ustuqtoplem  22775  utopsnneiplem  22783  utopsnnei  22785  utopreg  22788  fmucnd  22828  neipcfilu  22832  imasdsf1olem  22910  xpsdsval  22918  met1stc  23058  metustel  23087  metustsym  23092  metuel2  23102  metustbl  23103  restmetu  23107  xrtgioo  23341  minveclem3b  23958  uniioombllem3  24113  dvivth  24534  gausslemma2dlem1a  25868  elimampt  30311  acunirnmpt  30332  acunirnmpt2  30333  acunirnmpt2f  30334  fnpreimac  30344  trsp2cyc  30692  locfinreflem  31003  ordtconnlem1  31066  esumcst  31221  esumrnmpt2  31226  measdivcstALTV  31383  oms0  31454  omssubadd  31457  cvmsss2  32418  poimirlem16  34789  poimirlem19  34792  poimirlem24  34797  poimirlem27  34800  itg2addnclem2  34825  nelrnmpt  41225  suprnmpt  41306  rnmptpr  41309  elrnmptd  41316  wessf1ornlem  41321  disjrnmpt2  41325  disjf1o  41328  disjinfi  41330  choicefi  41339  rnmptlb  41390  rnmptbddlem  41391  rnmptbd2lem  41396  infnsuprnmpt  41398  elmptima  41406  supxrleubrnmpt  41555  suprleubrnmpt  41572  infrnmptle  41573  infxrunb3rnmpt  41578  supminfrnmpt  41595  infxrgelbrnmpt  41606  infrpgernmpt  41617  supminfxrrnmpt  41623  stoweidlem27  42189  stoweidlem31  42193  stoweidlem35  42197  stirlinglem5  42240  stirlinglem13  42248  fourierdlem53  42321  fourierdlem80  42348  fourierdlem93  42361  fourierdlem103  42371  fourierdlem104  42372  subsaliuncllem  42517  subsaliuncl  42518  sge0rnn0  42527  sge00  42535  fsumlesge0  42536  sge0tsms  42539  sge0cl  42540  sge0f1o  42541  sge0fsum  42546  sge0supre  42548  sge0rnbnd  42552  sge0pnffigt  42555  sge0lefi  42557  sge0ltfirp  42559  sge0resplit  42565  sge0split  42568  sge0reuz  42606  sge0reuzb  42607  hoidmvlelem2  42755  smfpimcc  42959
  Copyright terms: Public domain W3C validator