Theorem fnmpt 6690

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3061  Vcvv 3474   ↦ cmpt 5231   Fn wfn 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-fun 6545  df-fn 6546

This theorem is referenced by:  fnmptd  6691  mpt0  6692  fnmptfvd  7042  ralrnmptw  7095  ralrnmpt  7097  fmpt  7109  fmpt2d  7122  f1ocnvd  7656  offval2  7689  ofrfval2  7690  fsplitfpar  8103  mptelixpg  8928  fifo  9426  cantnflem1  9683  infmap2  10212  compssiso  10368  gruiun  10793  mptnn0fsupp  13961  mptnn0fsuppr  13963  seqof  14024  rlimi2  15457  prdsbas3  17426  prdsbascl  17428  prdsdsval2  17429  quslem  17488  fnmrc  17550  isofn  17721  pmtrrn  19324  pmtrfrn  19325  pmtrdifwrdellem2  19349  gsummptcl  19834  mptscmfsupp0  20536  ofco2  21952  pmatcollpw2lem  22278  neif  22603  tgrest  22662  cmpfi  22911  elptr2  23077  xkoptsub  23157  ptcmplem2  23556  ptcmplem3  23557  prdsxmetlem  23873  prdsxmslem2  24037  bcth3  24847  uniioombllem6  25104  itg2const  25257  ellimc2  25393  dvrec  25471  dvmptres3  25472  ulmss  25908  ulmdvlem1  25911  ulmdvlem2  25912  ulmdvlem3  25913  itgulm2  25920  psercn  25937  tgjustr  27722  f1o3d  31846  f1od2  31941  psgnfzto1stlem  32254  ghmquskerco  32524  frlmdim  32691  rmulccn  32903  esumnul  33041  esum0  33042  gsumesum  33052  ofcfval2  33097  signsplypnf  33556  signsply0  33557  hgt750lemb  33663  gg-rmulccn  35174  matunitlindflem1  36479  matunitlindflem2  36480  cdlemk56  39837  dicfnN  40049  hbtlem7  41857  refsumcn  43704  wessf1ornlem  43872  choicefi  43889  axccdom  43911  fsumsermpt  44285  liminfval2  44474  stoweidlem31  44737  stoweidlem59  44765  stirlinglem13  44792  dirkercncflem2  44810  fourierdlem62  44874  subsaliuncllem  45063  subsaliuncl  45064  hoidmvlelem3  45303  dfafn5b  45859  fundcmpsurinjlem2  46057  lincresunit2  47149