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

Theorem fnmpt 6637
Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)
Hypothesis
Ref Expression
mptfng.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
fnmpt (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fnmpt
StepHypRef Expression
1 elex 3462 . . 3 (𝐵𝑉𝐵 ∈ V)
21ralimi 3085 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 mptfng.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6636 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4sylib 217 1 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  wral 3063  Vcvv 3444  cmpt 5187   Fn wfn 6487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6494  df-fn 6495
This theorem is referenced by:  fnmptd  6638  mpt0  6639  fnmptfvd  6987  ralrnmptw  7039  ralrnmpt  7041  fmpt  7053  fmpt2d  7066  f1ocnvd  7595  offval2  7628  ofrfval2  7629  fsplitfpar  8039  mptelixpg  8807  fifo  9302  cantnflem1  9559  infmap2  10088  compssiso  10244  gruiun  10669  mptnn0fsupp  13832  mptnn0fsuppr  13834  seqof  13895  rlimi2  15332  prdsbas3  17299  prdsbascl  17301  prdsdsval2  17302  quslem  17361  fnmrc  17423  isofn  17594  pmtrrn  19174  pmtrfrn  19175  pmtrdifwrdellem2  19199  gsummptcl  19679  mptscmfsupp0  20316  ofco2  21728  pmatcollpw2lem  22054  neif  22379  tgrest  22438  cmpfi  22687  elptr2  22853  xkoptsub  22933  ptcmplem2  23332  ptcmplem3  23333  prdsxmetlem  23649  prdsxmslem2  23813  bcth3  24623  uniioombllem6  24880  itg2const  25033  ellimc2  25169  dvrec  25247  dvmptres3  25248  ulmss  25684  ulmdvlem1  25687  ulmdvlem2  25688  ulmdvlem3  25689  itgulm2  25696  psercn  25713  tgjustr  27221  f1o3d  31345  f1od2  31439  psgnfzto1stlem  31750  frlmdim  32098  rmulccn  32289  esumnul  32427  esum0  32428  gsumesum  32438  ofcfval2  32483  signsplypnf  32942  signsply0  32943  hgt750lemb  33049  matunitlindflem1  36005  matunitlindflem2  36006  cdlemk56  39365  dicfnN  39577  hbtlem7  41354  refsumcn  43036  wessf1ornlem  43198  choicefi  43216  axccdom  43238  fsumsermpt  43611  liminfval2  43800  stoweidlem31  44063  stoweidlem59  44091  stirlinglem13  44118  dirkercncflem2  44136  fourierdlem62  44200  subsaliuncllem  44389  subsaliuncl  44390  hoidmvlelem3  44629  dfafn5b  45184  fundcmpsurinjlem2  45382  lincresunit2  46350
  Copyright terms: Public domain W3C validator