Theorem fnmpt 6557

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Vcvv 3422   ↦ cmpt 5153   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-fun 6420  df-fn 6421

This theorem is referenced by:  fnmptd  6558  mpt0  6559  fnmptfvd  6900  ralrnmptw  6952  ralrnmpt  6954  fmpt  6966  fmpt2d  6979  f1ocnvd  7498  offval2  7531  ofrfval2  7532  fsplitfpar  7930  mptelixpg  8681  fifo  9121  cantnflem1  9377  infmap2  9905  compssiso  10061  gruiun  10486  mptnn0fsupp  13645  mptnn0fsuppr  13647  seqof  13708  rlimi2  15151  prdsbas3  17109  prdsbascl  17111  prdsdsval2  17112  quslem  17171  fnmrc  17233  isofn  17404  pmtrrn  18980  pmtrfrn  18981  pmtrdifwrdellem2  19005  gsummptcl  19483  mptscmfsupp0  20103  ofco2  21508  pmatcollpw2lem  21834  neif  22159  tgrest  22218  cmpfi  22467  elptr2  22633  xkoptsub  22713  ptcmplem2  23112  ptcmplem3  23113  prdsxmetlem  23429  prdsxmslem2  23591  bcth3  24400  uniioombllem6  24657  itg2const  24810  ellimc2  24946  dvrec  25024  dvmptres3  25025  ulmss  25461  ulmdvlem1  25464  ulmdvlem2  25465  ulmdvlem3  25466  itgulm2  25473  psercn  25490  tgjustr  26739  f1o3d  30863  f1od2  30958  psgnfzto1stlem  31269  frlmdim  31596  rmulccn  31780  esumnul  31916  esum0  31917  gsumesum  31927  ofcfval2  31972  signsplypnf  32429  signsply0  32430  hgt750lemb  32536  matunitlindflem1  35700  matunitlindflem2  35701  cdlemk56  38912  dicfnN  39124  hbtlem7  40866  refsumcn  42462  wessf1ornlem  42611  choicefi  42629  axccdom  42651  fsumsermpt  43010  liminfval2  43199  stoweidlem31  43462  stoweidlem59  43490  stirlinglem13  43517  dirkercncflem2  43535  fourierdlem62  43599  subsaliuncllem  43786  subsaliuncl  43787  hoidmvlelem3  44025  dfafn5b  44540  fundcmpsurinjlem2  44739  lincresunit2  45707