Theorem fnmpt 6661

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ↦ cmpt 5191   Fn wfn 6509

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-fun 6516  df-fn 6517

This theorem is referenced by:  fnmptd  6662  mpt0  6663  fnmptfvd  7016  ralrnmptw  7069  ralrnmpt  7071  fmpt  7085  fmpt2d  7099  f1ocnvd  7643  offval2  7676  ofrfval2  7677  mptcnfimad  7968  fsplitfpar  8100  mptelixpg  8911  fifo  9390  cantnflem1  9649  infmap2  10177  compssiso  10334  gruiun  10759  mptnn0fsupp  13969  mptnn0fsuppr  13971  seqof  14031  rlimi2  15487  prdsbas3  17451  prdsbascl  17453  prdsdsval2  17454  quslem  17513  fnmrc  17575  isofn  17744  ghmquskerco  19223  pmtrrn  19394  pmtrfrn  19395  pmtrdifwrdellem2  19419  gsummptcl  19904  mptscmfsupp0  20840  ofco2  22345  pmatcollpw2lem  22671  neif  22994  tgrest  23053  cmpfi  23302  elptr2  23468  xkoptsub  23548  ptcmplem2  23947  ptcmplem3  23948  prdsxmetlem  24263  prdsxmslem2  24424  bcth3  25238  uniioombllem6  25496  itg2const  25648  ellimc2  25785  dvrec  25866  dvmptres3  25867  ulmss  26313  ulmdvlem1  26316  ulmdvlem2  26317  ulmdvlem3  26318  itgulm2  26325  psercn  26343  tgjustr  28408  f1o3d  32558  f1od2  32651  psgnfzto1stlem  33064  frlmdim  33614  rmulccn  33925  esumnul  34045  esum0  34046  gsumesum  34056  ofcfval2  34101  signsplypnf  34548  signsply0  34549  hgt750lemb  34654  wevgblacfn  35103  matunitlindflem1  37617  matunitlindflem2  37618  cdlemk56  40972  dicfnN  41184  hbtlem7  43121  refsumcn  45031  wessf1ornlem  45186  choicefi  45201  axccdom  45223  fsumsermpt  45584  liminfval2  45773  stoweidlem31  46036  stoweidlem59  46064  stirlinglem13  46091  dirkercncflem2  46109  fourierdlem62  46173  subsaliuncllem  46362  subsaliuncl  46363  hoidmvlelem3  46602  dfafn5b  47166  fundcmpsurinjlem2  47404  upgrimwlklem1  47901  lincresunit2  48471  isofnALT  49024