Theorem fnmpt 6691

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ↦ cmpt 5232   Fn wfn 6539

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-fun 6546  df-fn 6547

This theorem is referenced by:  fnmptd  6692  mpt0  6693  fnmptfvd  7043  ralrnmptw  7096  ralrnmpt  7098  fmpt  7110  fmpt2d  7123  f1ocnvd  7657  offval2  7690  ofrfval2  7691  fsplitfpar  8104  mptelixpg  8929  fifo  9427  cantnflem1  9684  infmap2  10213  compssiso  10369  gruiun  10794  mptnn0fsupp  13962  mptnn0fsuppr  13964  seqof  14025  rlimi2  15458  prdsbas3  17427  prdsbascl  17429  prdsdsval2  17430  quslem  17489  fnmrc  17551  isofn  17722  pmtrrn  19325  pmtrfrn  19326  pmtrdifwrdellem2  19350  gsummptcl  19835  mptscmfsupp0  20537  ofco2  21953  pmatcollpw2lem  22279  neif  22604  tgrest  22663  cmpfi  22912  elptr2  23078  xkoptsub  23158  ptcmplem2  23557  ptcmplem3  23558  prdsxmetlem  23874  prdsxmslem2  24038  bcth3  24848  uniioombllem6  25105  itg2const  25258  ellimc2  25394  dvrec  25472  dvmptres3  25473  ulmss  25909  ulmdvlem1  25912  ulmdvlem2  25913  ulmdvlem3  25914  itgulm2  25921  psercn  25938  tgjustr  27725  f1o3d  31851  f1od2  31946  psgnfzto1stlem  32259  ghmquskerco  32529  frlmdim  32696  rmulccn  32908  esumnul  33046  esum0  33047  gsumesum  33057  ofcfval2  33102  signsplypnf  33561  signsply0  33562  hgt750lemb  33668  gg-rmulccn  35179  matunitlindflem1  36484  matunitlindflem2  36485  cdlemk56  39842  dicfnN  40054  hbtlem7  41867  refsumcn  43714  wessf1ornlem  43882  choicefi  43899  axccdom  43921  fsumsermpt  44295  liminfval2  44484  stoweidlem31  44747  stoweidlem59  44775  stirlinglem13  44802  dirkercncflem2  44820  fourierdlem62  44884  subsaliuncllem  45073  subsaliuncl  45074  hoidmvlelem3  45313  dfafn5b  45869  fundcmpsurinjlem2  46067  lincresunit2  47159