Theorem fnmpt 6661

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

Step	Hyp	Ref	Expression
1		elex 3475	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3099	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		mptfng.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6660	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	sylib 220	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∀wral 3076  Vcvv 3454   ↦ cmpt 5181   Fn wfn 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-fun 6523  df-fn 6524

This theorem is referenced by:  fnmptd  6662  mpt0  6663  fnmptfvd  7022  ralrnmptw  7075  ralrnmpt  7077  fmpt  7091  fmpt2d  7106  f1ocnvd  7647  offval2  7680  ofrfval2  7681  mptcnfimad  7967  fsplitfpar  8097  mptelixpg  8917  fifo  9378  cantnflem1  9644  infmap2  10173  compssiso  10331  gruiun  10757  mptnn0fsupp  14010  mptnn0fsuppr  14012  seqof  14072  sgnrn  15111  rlimi2  15541  prdsbas3  17510  prdsbascl  17512  prdsdsval2  17513  quslem  17573  fnmrc  17639  isofn  17808  ghmquskerco  19324  pmtrrn  19497  pmtrfrn  19498  pmtrdifwrdellem2  19522  gsummptcl  20007  mptscmfsupp0  20994  ofco2  22511  pmatcollpw2lem  22837  neif  23160  tgrest  23219  cmpfi  23468  elptr2  23634  xkoptsub  23714  ptcmplem2  24113  ptcmplem3  24114  prdsxmetlem  24428  prdsxmslem2  24589  bcth3  25393  uniioombllem6  25650  itg2const  25802  ellimc2  25939  dvrec  26017  dvmptres3  26018  ulmss  26460  ulmdvlem1  26463  ulmdvlem2  26464  ulmdvlem3  26465  itgulm2  26472  psercn  26489  tgjustr  28643  f1o3d  32828  f1od2  32921  psgnfzto1stlem  33280  frlmdim  33908  rmulccn  34225  esumnul  34345  esum0  34346  gsumesum  34356  ofcfval2  34401  signsplypnf  34844  signsply0  34845  hgt750lemb  34950  fineqvnttrclse  35420  wevgblacfn  35454  matunitlindflem1  38115  matunitlindflem2  38116  cdlemk56  41595  dicfnN  41807  hbtlem7  43702  refsumcn  45610  wessf1ornlem  45763  choicefi  45777  axccdom  45798  fsumsermpt  46155  liminfval2  46342  stoweidlem31  46605  stoweidlem59  46633  stirlinglem13  46660  dirkercncflem2  46678  fourierdlem62  46742  subsaliuncllem  46931  subsaliuncl  46932  hoidmvlelem3  47171  dfafn5b  47755  fundcmpsurinjlem2  48005  upgrimwlklem1  48519  lincresunit2  49100  isofnALT  49652