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

Theorem fnmpt 6642
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 3083 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 mptfng.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6641 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4sylib 217 1 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  wral 3061  Vcvv 3444  cmpt 5189   Fn wfn 6492
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 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-fun 6499  df-fn 6500
This theorem is referenced by:  fnmptd  6643  mpt0  6644  fnmptfvd  6992  ralrnmptw  7045  ralrnmpt  7047  fmpt  7059  fmpt2d  7072  f1ocnvd  7605  offval2  7638  ofrfval2  7639  fsplitfpar  8051  mptelixpg  8876  fifo  9373  cantnflem1  9630  infmap2  10159  compssiso  10315  gruiun  10740  mptnn0fsupp  13908  mptnn0fsuppr  13910  seqof  13971  rlimi2  15402  prdsbas3  17368  prdsbascl  17370  prdsdsval2  17371  quslem  17430  fnmrc  17492  isofn  17663  pmtrrn  19244  pmtrfrn  19245  pmtrdifwrdellem2  19269  gsummptcl  19749  mptscmfsupp0  20402  ofco2  21816  pmatcollpw2lem  22142  neif  22467  tgrest  22526  cmpfi  22775  elptr2  22941  xkoptsub  23021  ptcmplem2  23420  ptcmplem3  23421  prdsxmetlem  23737  prdsxmslem2  23901  bcth3  24711  uniioombllem6  24968  itg2const  25121  ellimc2  25257  dvrec  25335  dvmptres3  25336  ulmss  25772  ulmdvlem1  25775  ulmdvlem2  25776  ulmdvlem3  25777  itgulm2  25784  psercn  25801  tgjustr  27458  f1o3d  31587  f1od2  31685  psgnfzto1stlem  31998  ghmquskerco  32244  frlmdim  32363  rmulccn  32566  esumnul  32704  esum0  32705  gsumesum  32715  ofcfval2  32760  signsplypnf  33219  signsply0  33220  hgt750lemb  33326  matunitlindflem1  36120  matunitlindflem2  36121  cdlemk56  39480  dicfnN  39692  hbtlem7  41495  refsumcn  43323  wessf1ornlem  43491  choicefi  43508  axccdom  43530  fsumsermpt  43906  liminfval2  44095  stoweidlem31  44358  stoweidlem59  44386  stirlinglem13  44413  dirkercncflem2  44431  fourierdlem62  44495  subsaliuncllem  44684  subsaliuncl  44685  hoidmvlelem3  44924  dfafn5b  45479  fundcmpsurinjlem2  45677  lincresunit2  46645
  Copyright terms: Public domain W3C validator