Theorem fnmpt 6573

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 3450	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3087	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		mptfng.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6572	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	sylib 217	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432   ↦ cmpt 5157   Fn wfn 6428

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-fun 6435  df-fn 6436

This theorem is referenced by:  fnmptd  6574  mpt0  6575  fnmptfvd  6918  ralrnmptw  6970  ralrnmpt  6972  fmpt  6984  fmpt2d  6997  f1ocnvd  7520  offval2  7553  ofrfval2  7554  fsplitfpar  7959  mptelixpg  8723  fifo  9191  cantnflem1  9447  infmap2  9974  compssiso  10130  gruiun  10555  mptnn0fsupp  13717  mptnn0fsuppr  13719  seqof  13780  rlimi2  15223  prdsbas3  17192  prdsbascl  17194  prdsdsval2  17195  quslem  17254  fnmrc  17316  isofn  17487  pmtrrn  19065  pmtrfrn  19066  pmtrdifwrdellem2  19090  gsummptcl  19568  mptscmfsupp0  20188  ofco2  21600  pmatcollpw2lem  21926  neif  22251  tgrest  22310  cmpfi  22559  elptr2  22725  xkoptsub  22805  ptcmplem2  23204  ptcmplem3  23205  prdsxmetlem  23521  prdsxmslem2  23685  bcth3  24495  uniioombllem6  24752  itg2const  24905  ellimc2  25041  dvrec  25119  dvmptres3  25120  ulmss  25556  ulmdvlem1  25559  ulmdvlem2  25560  ulmdvlem3  25561  itgulm2  25568  psercn  25585  tgjustr  26835  f1o3d  30962  f1od2  31056  psgnfzto1stlem  31367  frlmdim  31694  rmulccn  31878  esumnul  32016  esum0  32017  gsumesum  32027  ofcfval2  32072  signsplypnf  32529  signsply0  32530  hgt750lemb  32636  matunitlindflem1  35773  matunitlindflem2  35774  cdlemk56  38985  dicfnN  39197  hbtlem7  40950  refsumcn  42573  wessf1ornlem  42722  choicefi  42740  axccdom  42762  fsumsermpt  43120  liminfval2  43309  stoweidlem31  43572  stoweidlem59  43600  stirlinglem13  43627  dirkercncflem2  43645  fourierdlem62  43709  subsaliuncllem  43896  subsaliuncl  43897  hoidmvlelem3  44135  dfafn5b  44653  fundcmpsurinjlem2  44851  lincresunit2  45819