Theorem fnmpt 6518

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  ∀wral 3061  Vcvv 3408   ↦ cmpt 5135   Fn wfn 6375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-fun 6382  df-fn 6383

This theorem is referenced by:  fnmptd  6519  mpt0  6520  fnmptfvd  6861  ralrnmptw  6913  ralrnmpt  6915  fmpt  6927  fmpt2d  6940  f1ocnvd  7456  offval2  7488  ofrfval2  7489  fsplitfpar  7887  mptelixpg  8616  fifo  9048  cantnflem1  9304  infmap2  9832  compssiso  9988  gruiun  10413  mptnn0fsupp  13570  mptnn0fsuppr  13572  seqof  13633  rlimi2  15075  prdsbas3  16986  prdsbascl  16988  prdsdsval2  16989  quslem  17048  fnmrc  17110  isofn  17280  pmtrrn  18849  pmtrfrn  18850  pmtrdifwrdellem2  18874  gsummptcl  19352  mptscmfsupp0  19964  ofco2  21348  pmatcollpw2lem  21674  neif  21997  tgrest  22056  cmpfi  22305  elptr2  22471  xkoptsub  22551  ptcmplem2  22950  ptcmplem3  22951  prdsxmetlem  23266  prdsxmslem2  23427  bcth3  24228  uniioombllem6  24485  itg2const  24638  ellimc2  24774  dvrec  24852  dvmptres3  24853  ulmss  25289  ulmdvlem1  25292  ulmdvlem2  25293  ulmdvlem3  25294  itgulm2  25301  psercn  25318  tgjustr  26565  f1o3d  30681  f1od2  30776  psgnfzto1stlem  31086  frlmdim  31408  rmulccn  31592  esumnul  31728  esum0  31729  gsumesum  31739  ofcfval2  31784  signsplypnf  32241  signsply0  32242  hgt750lemb  32348  matunitlindflem1  35510  matunitlindflem2  35511  cdlemk56  38722  dicfnN  38934  hbtlem7  40653  refsumcn  42246  wessf1ornlem  42395  choicefi  42413  axccdom  42435  fsumsermpt  42795  liminfval2  42984  stoweidlem31  43247  stoweidlem59  43275  stirlinglem13  43302  dirkercncflem2  43320  fourierdlem62  43384  subsaliuncllem  43571  subsaliuncl  43572  hoidmvlelem3  43810  dfafn5b  44325  fundcmpsurinjlem2  44524  lincresunit2  45492