Theorem fnmpt 6621

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∀wral 3047  Vcvv 3436   ↦ cmpt 5170   Fn wfn 6476

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-fun 6483  df-fn 6484

This theorem is referenced by:  fnmptd  6622  mpt0  6623  fnmptfvd  6974  ralrnmptw  7027  ralrnmpt  7029  fmpt  7043  fmpt2d  7057  f1ocnvd  7597  offval2  7630  ofrfval2  7631  mptcnfimad  7918  fsplitfpar  8048  mptelixpg  8859  fifo  9316  cantnflem1  9579  infmap2  10108  compssiso  10265  gruiun  10690  mptnn0fsupp  13904  mptnn0fsuppr  13906  seqof  13966  rlimi2  15421  prdsbas3  17385  prdsbascl  17387  prdsdsval2  17388  quslem  17447  fnmrc  17513  isofn  17682  ghmquskerco  19196  pmtrrn  19369  pmtrfrn  19370  pmtrdifwrdellem2  19394  gsummptcl  19879  mptscmfsupp0  20860  ofco2  22366  pmatcollpw2lem  22692  neif  23015  tgrest  23074  cmpfi  23323  elptr2  23489  xkoptsub  23569  ptcmplem2  23968  ptcmplem3  23969  prdsxmetlem  24283  prdsxmslem2  24444  bcth3  25258  uniioombllem6  25516  itg2const  25668  ellimc2  25805  dvrec  25886  dvmptres3  25887  ulmss  26333  ulmdvlem1  26336  ulmdvlem2  26337  ulmdvlem3  26338  itgulm2  26345  psercn  26363  tgjustr  28452  f1o3d  32608  f1od2  32702  psgnfzto1stlem  33069  frlmdim  33624  rmulccn  33941  esumnul  34061  esum0  34062  gsumesum  34072  ofcfval2  34117  signsplypnf  34563  signsply0  34564  hgt750lemb  34669  fineqvnttrclse  35144  wevgblacfn  35153  matunitlindflem1  37666  matunitlindflem2  37667  cdlemk56  41080  dicfnN  41292  hbtlem7  43228  refsumcn  45137  wessf1ornlem  45292  choicefi  45307  axccdom  45329  fsumsermpt  45689  liminfval2  45876  stoweidlem31  46139  stoweidlem59  46167  stirlinglem13  46194  dirkercncflem2  46212  fourierdlem62  46276  subsaliuncllem  46465  subsaliuncl  46466  hoidmvlelem3  46705  dfafn5b  47271  fundcmpsurinjlem2  47509  upgrimwlklem1  48007  lincresunit2  48589  isofnALT  49142