Theorem fnmpt 6673

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

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

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 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6535  df-fn 6536

This theorem is used by:  fnmptd  6674  mpt0  6675  fnmptfvd  7034  ralrnmptw  7088  ralrnmpt  7090  fmpt  7104  fmpt2d  7119  f1ocnvd  7666  offval2  7699  ofrfval2  7700  mptcnfimad  7984  fsplitfpar  8116  mptelixpg  8945  fifo  9405  cantnflem1  9671  infmap2  10222  compssiso  10379  gruiun  10811  mptnn0fsupp  14064  mptnn0fsuppr  14066  seqof  14126  sgnrn  15174  rlimi2  15604  prdsbas3  17569  prdsbascl  17571  prdsdsval2  17572  quslem  17632  fnmrc  17698  isofn  17867  ghmquskerco  19414  pmtrrn  19587  pmtrfrn  19588  pmtrdifwrdellem2  19612  gsummptcl  20097  mptscmfsupp0  21114  ofco2  22676  matunitlindflem1  22904  matunitlindflem2  22905  pmatcollpw2lem  23005  neif  23328  tgrest  23387  cmpfi  23636  elptr2  23803  xkoptsub  23883  ptcmplem2  24282  ptcmplem3  24283  prdsxmetlem  24597  prdsxmslem2  24758  bcth3  25562  uniioombllem6  25819  itg2const  25971  ellimc2  26107  dvrec  26185  dvmptres3  26186  ulmss  26636  ulmdvlem1  26639  ulmdvlem2  26640  ulmdvlem3  26641  itgulm2  26648  psercn  26665  tgjustr  28818  f1o3d  33102  f1od2  33193  psgnfzto1stlem  33543  frlmdim  34124  rmulccn  34441  esumnul  34561  esum0  34562  gsumesum  34572  ofcfval2  34617  signsplypnf  35061  signsply0  35062  hgt750lemb  35167  fineqvnttrclse  35653  wevgblacfn  35711  cdlemk56  41847  dicfnN  42059  hbtlem7  43969  refsumcn  45867  wessf1ornlem  46020  choicefi  46034  axccdom  46055  fsumsermpt  46412  liminfval2  46599  stoweidlem31  46862  stoweidlem59  46890  stirlinglem13  46917  dirkercncflem2  46935  fourierdlem62  46999  subsaliuncllem  47188  subsaliuncl  47189  hoidmvlelem3  47428  dfafn5b  48052  fundcmpsurinjlem2  48302  upgrimwlklem1  48816  lincresunit2  49411  isofnALT  49960