Theorem fnmpt 6708

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   ↦ cmpt 5225   Fn wfn 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-fun 6563  df-fn 6564

This theorem is referenced by:  fnmptd  6709  mpt0  6710  fnmptfvd  7061  ralrnmptw  7114  ralrnmpt  7116  fmpt  7130  fmpt2d  7144  f1ocnvd  7684  offval2  7717  ofrfval2  7718  mptcnfimad  8011  fsplitfpar  8143  mptelixpg  8975  fifo  9472  cantnflem1  9729  infmap2  10257  compssiso  10414  gruiun  10839  mptnn0fsupp  14038  mptnn0fsuppr  14040  seqof  14100  rlimi2  15550  prdsbas3  17526  prdsbascl  17528  prdsdsval2  17529  quslem  17588  fnmrc  17650  isofn  17819  ghmquskerco  19302  pmtrrn  19475  pmtrfrn  19476  pmtrdifwrdellem2  19500  gsummptcl  19985  mptscmfsupp0  20925  ofco2  22457  pmatcollpw2lem  22783  neif  23108  tgrest  23167  cmpfi  23416  elptr2  23582  xkoptsub  23662  ptcmplem2  24061  ptcmplem3  24062  prdsxmetlem  24378  prdsxmslem2  24542  bcth3  25365  uniioombllem6  25623  itg2const  25775  ellimc2  25912  dvrec  25993  dvmptres3  25994  ulmss  26440  ulmdvlem1  26443  ulmdvlem2  26444  ulmdvlem3  26445  itgulm2  26452  psercn  26470  tgjustr  28482  f1o3d  32637  f1od2  32732  psgnfzto1stlem  33120  frlmdim  33662  rmulccn  33927  esumnul  34049  esum0  34050  gsumesum  34060  ofcfval2  34105  signsplypnf  34565  signsply0  34566  hgt750lemb  34671  wevgblacfn  35114  matunitlindflem1  37623  matunitlindflem2  37624  cdlemk56  40973  dicfnN  41185  hbtlem7  43137  refsumcn  45035  wessf1ornlem  45190  choicefi  45205  axccdom  45227  fsumsermpt  45594  liminfval2  45783  stoweidlem31  46046  stoweidlem59  46074  stirlinglem13  46101  dirkercncflem2  46119  fourierdlem62  46183  subsaliuncllem  46372  subsaliuncl  46373  hoidmvlelem3  46612  dfafn5b  47173  fundcmpsurinjlem2  47386  lincresunit2  48395