Theorem fnmpt 6658

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447   ↦ cmpt 5188   Fn wfn 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  fnmptd  6659  mpt0  6660  fnmptfvd  7013  ralrnmptw  7066  ralrnmpt  7068  fmpt  7082  fmpt2d  7096  f1ocnvd  7640  offval2  7673  ofrfval2  7674  mptcnfimad  7965  fsplitfpar  8097  mptelixpg  8908  fifo  9383  cantnflem1  9642  infmap2  10170  compssiso  10327  gruiun  10752  mptnn0fsupp  13962  mptnn0fsuppr  13964  seqof  14024  rlimi2  15480  prdsbas3  17444  prdsbascl  17446  prdsdsval2  17447  quslem  17506  fnmrc  17568  isofn  17737  ghmquskerco  19216  pmtrrn  19387  pmtrfrn  19388  pmtrdifwrdellem2  19412  gsummptcl  19897  mptscmfsupp0  20833  ofco2  22338  pmatcollpw2lem  22664  neif  22987  tgrest  23046  cmpfi  23295  elptr2  23461  xkoptsub  23541  ptcmplem2  23940  ptcmplem3  23941  prdsxmetlem  24256  prdsxmslem2  24417  bcth3  25231  uniioombllem6  25489  itg2const  25641  ellimc2  25778  dvrec  25859  dvmptres3  25860  ulmss  26306  ulmdvlem1  26309  ulmdvlem2  26310  ulmdvlem3  26311  itgulm2  26318  psercn  26336  tgjustr  28401  f1o3d  32551  f1od2  32644  psgnfzto1stlem  33057  frlmdim  33607  rmulccn  33918  esumnul  34038  esum0  34039  gsumesum  34049  ofcfval2  34094  signsplypnf  34541  signsply0  34542  hgt750lemb  34647  wevgblacfn  35096  matunitlindflem1  37610  matunitlindflem2  37611  cdlemk56  40965  dicfnN  41177  hbtlem7  43114  refsumcn  45024  wessf1ornlem  45179  choicefi  45194  axccdom  45216  fsumsermpt  45577  liminfval2  45766  stoweidlem31  46029  stoweidlem59  46057  stirlinglem13  46084  dirkercncflem2  46102  fourierdlem62  46166  subsaliuncllem  46355  subsaliuncl  46356  hoidmvlelem3  46595  dfafn5b  47162  fundcmpsurinjlem2  47400  upgrimwlklem1  47897  lincresunit2  48467  isofnALT  49020