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 3478	. . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3104	. 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 2146  ∀wral 3081  Vcvv 3457   ↦ cmpt 5194   Fn wfn 6535

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6542  df-fn 6543

This theorem is used by:  fnmptd  6680  mpt0  6681  fnmptfvd  7040  ralrnmptw  7093  ralrnmpt  7095  fmpt  7109  fmpt2d  7124  f1ocnvd  7671  offval2  7704  ofrfval2  7705  mptcnfimad  7989  fsplitfpar  8119  mptelixpg  8939  fifo  9399  cantnflem1  9665  infmap2  10216  compssiso  10373  gruiun  10801  mptnn0fsupp  14053  mptnn0fsuppr  14055  seqof  14115  sgnrn  15161  rlimi2  15591  prdsbas3  17558  prdsbascl  17560  prdsdsval2  17561  quslem  17621  fnmrc  17687  isofn  17856  ghmquskerco  19400  pmtrrn  19573  pmtrfrn  19574  pmtrdifwrdellem2  19598  gsummptcl  20083  mptscmfsupp0  21100  ofco2  22660  pmatcollpw2lem  22986  neif  23309  tgrest  23368  cmpfi  23617  elptr2  23784  xkoptsub  23864  ptcmplem2  24263  ptcmplem3  24264  prdsxmetlem  24578  prdsxmslem2  24739  bcth3  25543  uniioombllem6  25800  itg2const  25952  ellimc2  26089  dvrec  26167  dvmptres3  26168  ulmss  26613  ulmdvlem1  26616  ulmdvlem2  26617  ulmdvlem3  26618  itgulm2  26625  psercn  26642  tgjustr  28796  f1o3d  33044  f1od2  33136  psgnfzto1stlem  33486  frlmdim  34067  rmulccn  34384  esumnul  34504  esum0  34505  gsumesum  34515  ofcfval2  34560  signsplypnf  35004  signsply0  35005  hgt750lemb  35110  fineqvnttrclse  35596  wevgblacfn  35654  matunitlindflem1  38326  matunitlindflem2  38327  cdlemk56  41805  dicfnN  42017  hbtlem7  43912  refsumcn  45810  wessf1ornlem  45963  choicefi  45977  axccdom  45998  fsumsermpt  46355  liminfval2  46542  stoweidlem31  46805  stoweidlem59  46833  stirlinglem13  46860  dirkercncflem2  46878  fourierdlem62  46942  subsaliuncllem  47131  subsaliuncl  47132  hoidmvlelem3  47371  dfafn5b  47958  fundcmpsurinjlem2  48208  upgrimwlklem1  48722  lincresunit2  49317  isofnALT  49868