Theorem fnmpt 6488

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3138  Vcvv 3494   ↦ cmpt 5146   Fn wfn 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-fun 6357  df-fn 6358

This theorem is referenced by:  fnmptd  6489  mpt0  6490  fnmptfvd  6811  ralrnmptw  6860  ralrnmpt  6862  fmpt  6874  fmpt2d  6887  f1ocnvd  7396  offval2  7426  ofrfval2  7427  fsplitfpar  7814  mptelixpg  8499  fifo  8896  cantnflem1  9152  infmap2  9640  compssiso  9796  gruiun  10221  mptnn0fsupp  13366  mptnn0fsuppr  13368  seqof  13428  rlimi2  14871  prdsbas3  16754  prdsbascl  16756  prdsdsval2  16757  quslem  16816  fnmrc  16878  isofn  17045  pmtrrn  18585  pmtrfrn  18586  pmtrdifwrdellem2  18610  gsummptcl  19087  mptscmfsupp0  19699  ofco2  21060  pmatcollpw2lem  21385  neif  21708  tgrest  21767  cmpfi  22016  elptr2  22182  xkoptsub  22262  ptcmplem2  22661  ptcmplem3  22662  prdsxmetlem  22978  prdsxmslem2  23139  bcth3  23934  uniioombllem6  24189  itg2const  24341  ellimc2  24475  dvrec  24552  dvmptres3  24553  ulmss  24985  ulmdvlem1  24988  ulmdvlem2  24989  ulmdvlem3  24990  itgulm2  24997  psercn  25014  tgjustr  26260  f1o3d  30372  f1od2  30457  psgnfzto1stlem  30742  frlmdim  31009  rmulccn  31171  esumnul  31307  esum0  31308  gsumesum  31318  ofcfval2  31363  signsplypnf  31820  signsply0  31821  hgt750lemb  31927  matunitlindflem1  34903  matunitlindflem2  34904  cdlemk56  38122  dicfnN  38334  hbtlem7  39774  refsumcn  41336  wessf1ornlem  41494  choicefi  41512  axccdom  41536  fsumsermpt  41909  liminfval2  42098  stoweidlem31  42365  stoweidlem59  42393  stirlinglem13  42420  dirkercncflem2  42438  fourierdlem62  42502  subsaliuncllem  42689  subsaliuncl  42690  hoidmvlelem3  42928  dfafn5b  43409  fundcmpsurinjlem2  43608  lincresunit2  44582