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

Theorem fnmpt 6487
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 3518 . . 3 (𝐵𝑉𝐵 ∈ V)
21ralimi 3165 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 mptfng.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6486 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4sylib 219 1 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  wral 3143  Vcvv 3500  cmpt 5143   Fn wfn 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-fun 6356  df-fn 6357
This theorem is referenced by:  fnmptd  6488  mpt0  6489  fnmptfvd  6809  ralrnmptw  6858  ralrnmpt  6860  fmpt  6872  fmpt2d  6885  f1ocnvd  7390  offval2  7420  ofrfval2  7421  fsplitfpar  7810  mptelixpg  8493  fifo  8890  cantnflem1  9146  infmap2  9634  compssiso  9790  gruiun  10215  mptnn0fsupp  13360  mptnn0fsuppr  13362  seqof  13422  rlimi2  14866  prdsbas3  16749  prdsbascl  16751  prdsdsval2  16752  quslem  16811  fnmrc  16873  isofn  17040  pmtrrn  18521  pmtrfrn  18522  pmtrdifwrdellem2  18546  gsummptcl  19023  mptscmfsupp0  19635  ofco2  20995  pmatcollpw2lem  21320  neif  21643  tgrest  21702  cmpfi  21951  elptr2  22117  xkoptsub  22197  ptcmplem2  22596  ptcmplem3  22597  prdsxmetlem  22912  prdsxmslem2  23073  bcth3  23868  uniioombllem6  24123  itg2const  24275  ellimc2  24409  dvrec  24486  dvmptres3  24487  ulmss  24919  ulmdvlem1  24922  ulmdvlem2  24923  ulmdvlem3  24924  itgulm2  24931  psercn  24948  tgjustr  26193  f1o3d  30306  f1od2  30389  psgnfzto1stlem  30675  frlmdim  30914  rmulccn  31076  esumnul  31212  esum0  31213  gsumesum  31223  ofcfval2  31268  signsplypnf  31725  signsply0  31726  hgt750lemb  31832  matunitlindflem1  34774  matunitlindflem2  34775  cdlemk56  37993  dicfnN  38205  hbtlem7  39609  refsumcn  41171  wessf1ornlem  41329  choicefi  41347  axccdom  41371  fsumsermpt  41744  liminfval2  41933  stoweidlem31  42201  stoweidlem59  42229  stirlinglem13  42256  dirkercncflem2  42274  fourierdlem62  42338  subsaliuncllem  42525  subsaliuncl  42526  hoidmvlelem3  42764  dfafn5b  43245  lincresunit2  44435
  Copyright terms: Public domain W3C validator