Theorem fnmpt 6675

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ↦ cmpt 5192   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-fun 6538  df-fn 6539

This theorem is referenced by:  fnmptd  6676  mpt0  6677  fnmptfvd  7036  ralrnmptw  7089  ralrnmpt  7091  fmpt  7105  fmpt2d  7120  f1ocnvd  7661  offval2  7694  ofrfval2  7695  mptcnfimad  7979  fsplitfpar  8109  mptelixpg  8929  fifo  9388  cantnflem1  9654  infmap2  10196  compssiso  10353  gruiun  10779  mptnn0fsupp  14029  mptnn0fsuppr  14031  seqof  14091  sgnrn  15131  rlimi2  15561  prdsbas3  17529  prdsbascl  17531  prdsdsval2  17532  quslem  17592  fnmrc  17658  isofn  17827  ghmquskerco  19349  pmtrrn  19522  pmtrfrn  19523  pmtrdifwrdellem2  19547  gsummptcl  20032  mptscmfsupp0  21048  ofco2  22608  pmatcollpw2lem  22934  neif  23257  tgrest  23316  cmpfi  23565  elptr2  23731  xkoptsub  23811  ptcmplem2  24210  ptcmplem3  24211  prdsxmetlem  24525  prdsxmslem2  24686  bcth3  25490  uniioombllem6  25747  itg2const  25899  ellimc2  26036  dvrec  26114  dvmptres3  26115  ulmss  26560  ulmdvlem1  26563  ulmdvlem2  26564  ulmdvlem3  26565  itgulm2  26572  psercn  26589  tgjustr  28743  f1o3d  32971  f1od2  33064  psgnfzto1stlem  33420  frlmdim  34001  rmulccn  34318  esumnul  34438  esum0  34439  gsumesum  34449  ofcfval2  34494  signsplypnf  34937  signsply0  34938  hgt750lemb  35043  fineqvnttrclse  35537  wevgblacfn  35595  matunitlindflem1  38287  matunitlindflem2  38288  cdlemk56  41765  dicfnN  41977  hbtlem7  43872  refsumcn  45770  wessf1ornlem  45923  choicefi  45937  axccdom  45958  fsumsermpt  46315  liminfval2  46502  stoweidlem31  46765  stoweidlem59  46793  stirlinglem13  46820  dirkercncflem2  46838  fourierdlem62  46902  subsaliuncllem  47091  subsaliuncl  47092  hoidmvlelem3  47331  dfafn5b  47918  fundcmpsurinjlem2  48168  upgrimwlklem1  48682  lincresunit2  49278  isofnALT  49829  crossp3i  50668