Theorem fnmpt 6687

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  ∀wral 3079  Vcvv 3453   ↦ cmpt 5188   Fn wfn 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  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 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-fun 6548  df-fn 6549

This theorem is used by:  fnmptd  6688  mpt0  6689  fnmptfvd  7048  ralrnmptw  7102  ralrnmpt  7104  fmpt  7118  fmpt2d  7133  f1ocnvd  7679  offval2  7720  ofrfval2  7721  mptcnfimad  8005  f1od2  8118  fsplitfpar  8139  mptelixpg  8974  fifo  9434  cantnflem1  9700  infmap2  10305  compssiso  10462  gruiun  10894  mptnn0fsupp  14150  mptnn0fsuppr  14152  seqof  14212  sgnrn  15263  rlimi2  15693  prdsbas3  17664  prdsbascl  17666  prdsdsval2  17667  quslem  17727  fnmrc  17793  isofn  17962  ghmquskerco  19510  pmtrrn  19683  pmtrfrn  19684  pmtrdifwrdellem2  19708  gsummptcl  20193  mptscmfsupp0  21214  ofco2  22778  matunitlindflem1  23006  matunitlindflem2  23007  pmatcollpw2lem  23107  neif  23430  tgrest  23489  cmpfi  23738  elptr2  23905  xkoptsub  23985  ptcmplem2  24384  ptcmplem3  24385  prdsxmetlem  24699  prdsxmslem2  24860  bcth3  25664  uniioombllem6  25921  itg2const  26073  ellimc2  26209  dvrec  26287  dvmptres3  26288  ulmss  26736  ulmdvlem1  26739  ulmdvlem2  26740  ulmdvlem3  26741  itgulm2  26748  psercn  26765  tgjustr  28948  f1o3d  33274  psgnfzto1stlem  33714  frlmdim  34296  rmulccn  34613  esumnul  34733  esum0  34734  gsumesum  34744  ofcfval2  34789  signsplypnf  35232  signsply0  35233  hgt750lemb  35338  fineqvnttrclse  35863  wevgblacfn  35993  mirimanoffr  36581  cdlemk56  42168  dicfnN  42380  hbtlem7  44267  refsumcn  46186  wessf1ornlem  46339  choicefi  46353  axccdom  46374  fsumsermpt  46730  liminfval2  46917  stoweidlem31  47180  stoweidlem59  47208  stirlinglem13  47235  dirkercncflem2  47253  fourierdlem62  47317  subsaliuncllem  47506  subsaliuncl  47507  hoidmvlelem3  47746  dfafn5b  48370  fundcmpsurinjlem2  48620  upgrimwlklem1  49134  lincresunit2  49729  isofnALT  50284