Theorem fnmpt 6678

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3051  Vcvv 3459   ↦ cmpt 5201   Fn wfn 6526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-fun 6533  df-fn 6534

This theorem is referenced by:  fnmptd  6679  mpt0  6680  fnmptfvd  7031  ralrnmptw  7084  ralrnmpt  7086  fmpt  7100  fmpt2d  7114  f1ocnvd  7658  offval2  7691  ofrfval2  7692  mptcnfimad  7985  fsplitfpar  8117  mptelixpg  8949  fifo  9444  cantnflem1  9703  infmap2  10231  compssiso  10388  gruiun  10813  mptnn0fsupp  14015  mptnn0fsuppr  14017  seqof  14077  rlimi2  15530  prdsbas3  17495  prdsbascl  17497  prdsdsval2  17498  quslem  17557  fnmrc  17619  isofn  17788  ghmquskerco  19267  pmtrrn  19438  pmtrfrn  19439  pmtrdifwrdellem2  19463  gsummptcl  19948  mptscmfsupp0  20884  ofco2  22389  pmatcollpw2lem  22715  neif  23038  tgrest  23097  cmpfi  23346  elptr2  23512  xkoptsub  23592  ptcmplem2  23991  ptcmplem3  23992  prdsxmetlem  24307  prdsxmslem2  24468  bcth3  25283  uniioombllem6  25541  itg2const  25693  ellimc2  25830  dvrec  25911  dvmptres3  25912  ulmss  26358  ulmdvlem1  26361  ulmdvlem2  26362  ulmdvlem3  26363  itgulm2  26370  psercn  26388  tgjustr  28453  f1o3d  32605  f1od2  32698  psgnfzto1stlem  33111  frlmdim  33651  rmulccn  33959  esumnul  34079  esum0  34080  gsumesum  34090  ofcfval2  34135  signsplypnf  34582  signsply0  34583  hgt750lemb  34688  wevgblacfn  35131  matunitlindflem1  37640  matunitlindflem2  37641  cdlemk56  40990  dicfnN  41202  hbtlem7  43149  refsumcn  45054  wessf1ornlem  45209  choicefi  45224  axccdom  45246  fsumsermpt  45608  liminfval2  45797  stoweidlem31  46060  stoweidlem59  46088  stirlinglem13  46115  dirkercncflem2  46133  fourierdlem62  46197  subsaliuncllem  46386  subsaliuncl  46387  hoidmvlelem3  46626  dfafn5b  47190  fundcmpsurinjlem2  47413  upgrimwlklem1  47910  lincresunit2  48454  isofnALT  49001