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

Theorem fnmpt 6058
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 3243 . . 3 (𝐵𝑉𝐵 ∈ V)
21ralimi 2981 . 2 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 mptfng.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6057 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4sylib 208 1 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231  cmpt 4762   Fn wfn 5921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-fun 5928  df-fn 5929
This theorem is referenced by:  mpt0  6059  fnmptfvd  6360  ralrnmpt  6408  fmpt  6421  fmpt2d  6433  f1ocnvd  6926  offval2  6956  ofrfval2  6957  mptelixpg  7987  fifo  8379  cantnflem1  8624  infmap2  9078  compssiso  9234  gruiun  9659  mptnn0fsupp  12837  mptnn0fsuppr  12839  seqof  12898  rlimi2  14289  prdsbas3  16188  prdsbascl  16190  prdsdsval2  16191  quslem  16250  fnmrc  16314  isofn  16482  pmtrrn  17923  pmtrfrn  17924  pmtrdifwrdellem2  17948  gsummptcl  18412  mptscmfsupp0  18976  ofco2  20305  pmatcollpw2lem  20630  neif  20952  tgrest  21011  cmpfi  21259  elptr2  21425  xkoptsub  21505  ptcmplem2  21904  ptcmplem3  21905  prdsxmetlem  22220  prdsxmslem2  22381  bcth3  23174  uniioombllem6  23402  itg2const  23552  ellimc2  23686  dvrec  23763  dvmptres3  23764  ulmss  24196  ulmdvlem1  24199  ulmdvlem2  24200  ulmdvlem3  24201  itgulm2  24208  psercn  24225  f1o3d  29559  f1od2  29627  psgnfzto1stlem  29978  rmulccn  30102  esumnul  30238  esum0  30239  gsumesum  30249  ofcfval2  30294  signsplypnf  30755  signsply0  30756  hgt750lemb  30862  matunitlindflem1  33535  matunitlindflem2  33536  cdlemk56  36576  dicfnN  36789  hbtlem7  38012  refsumcn  39503  wessf1ornlem  39685  choicefi  39706  axccdom  39730  fnmptd  39748  fsumsermpt  40129  liminfval2  40318  stoweidlem31  40566  stoweidlem59  40594  stirlinglem13  40621  dirkercncflem2  40639  fourierdlem62  40703  subsaliuncllem  40893  subsaliuncl  40894  hoidmvlelem3  41132  dfafn5b  41562  lincresunit2  42592
  Copyright terms: Public domain W3C validator