Theorem fnmpt 6679

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077  Vcvv 3451   ↦ cmpt 5186   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6540  df-fn 6541

This theorem is used by:  fnmptd  6680  mpt0  6681  fnmptfvd  7040  ralrnmptw  7094  ralrnmpt  7096  fmpt  7110  fmpt2d  7125  f1ocnvd  7672  offval2  7713  ofrfval2  7714  mptcnfimad  7998  fsplitfpar  8129  mptelixpg  8963  fifo  9424  cantnflem1  9690  infmap2  10295  compssiso  10452  gruiun  10884  mptnn0fsupp  14140  mptnn0fsuppr  14142  seqof  14202  sgnrn  15251  rlimi2  15681  prdsbas3  17652  prdsbascl  17654  prdsdsval2  17655  quslem  17715  fnmrc  17781  isofn  17950  ghmquskerco  19498  pmtrrn  19671  pmtrfrn  19672  pmtrdifwrdellem2  19696  gsummptcl  20181  mptscmfsupp0  21202  ofco2  22766  matunitlindflem1  22994  matunitlindflem2  22995  pmatcollpw2lem  23095  neif  23418  tgrest  23477  cmpfi  23726  elptr2  23893  xkoptsub  23973  ptcmplem2  24372  ptcmplem3  24373  prdsxmetlem  24687  prdsxmslem2  24848  bcth3  25652  uniioombllem6  25909  itg2const  26061  ellimc2  26197  dvrec  26275  dvmptres3  26276  ulmss  26724  ulmdvlem1  26727  ulmdvlem2  26728  ulmdvlem3  26729  itgulm2  26736  psercn  26753  tgjustr  28936  f1o3d  33220  f1od2  33311  psgnfzto1stlem  33661  frlmdim  34243  rmulccn  34560  esumnul  34680  esum0  34681  gsumesum  34691  ofcfval2  34736  signsplypnf  35179  signsply0  35180  hgt750lemb  35285  fineqvnttrclse  35792  wevgblacfn  35890  cdlemk56  42028  dicfnN  42240  hbtlem7  44126  refsumcn  46046  wessf1ornlem  46199  choicefi  46213  axccdom  46234  fsumsermpt  46590  liminfval2  46777  stoweidlem31  47040  stoweidlem59  47068  stirlinglem13  47095  dirkercncflem2  47113  fourierdlem62  47177  subsaliuncllem  47366  subsaliuncl  47367  hoidmvlelem3  47606  dfafn5b  48230  fundcmpsurinjlem2  48480  upgrimwlklem1  48994  lincresunit2  49589  isofnALT  50138