Theorem fnmpt 6676

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∀wral 3085  Vcvv 3463   ↦ cmpt 5196   Fn wfn 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-fun 6539  df-fn 6540

This theorem is referenced by:  fnmptd  6677  mpt0  6678  fnmptfvd  7037  ralrnmptw  7090  ralrnmpt  7092  fmpt  7106  fmpt2d  7121  f1ocnvd  7662  offval2  7695  ofrfval2  7696  mptcnfimad  7983  fsplitfpar  8113  mptelixpg  8933  fifo  9392  cantnflem1  9658  infmap2  10200  compssiso  10358  gruiun  10784  mptnn0fsupp  14033  mptnn0fsuppr  14035  seqof  14095  sgnrn  15135  rlimi2  15565  prdsbas3  17534  prdsbascl  17536  prdsdsval2  17537  quslem  17597  fnmrc  17663  isofn  17832  ghmquskerco  19354  pmtrrn  19527  pmtrfrn  19528  pmtrdifwrdellem2  19552  gsummptcl  20037  mptscmfsupp0  21026  ofco2  22577  pmatcollpw2lem  22903  neif  23226  tgrest  23285  cmpfi  23534  elptr2  23700  xkoptsub  23780  ptcmplem2  24179  ptcmplem3  24180  prdsxmetlem  24494  prdsxmslem2  24655  bcth3  25459  uniioombllem6  25716  itg2const  25868  ellimc2  26005  dvrec  26083  dvmptres3  26084  ulmss  26526  ulmdvlem1  26529  ulmdvlem2  26530  ulmdvlem3  26531  itgulm2  26538  psercn  26555  tgjustr  28709  f1o3d  32912  f1od2  33005  psgnfzto1stlem  33361  frlmdim  33946  rmulccn  34263  esumnul  34383  esum0  34384  gsumesum  34394  ofcfval2  34439  signsplypnf  34882  signsply0  34883  hgt750lemb  34988  fineqvnttrclse  35460  wevgblacfn  35494  matunitlindflem1  38155  matunitlindflem2  38156  cdlemk56  41635  dicfnN  41847  hbtlem7  43744  refsumcn  45642  wessf1ornlem  45795  choicefi  45809  axccdom  45830  fsumsermpt  46187  liminfval2  46374  stoweidlem31  46637  stoweidlem59  46665  stirlinglem13  46692  dirkercncflem2  46710  fourierdlem62  46774  subsaliuncllem  46963  subsaliuncl  46964  hoidmvlelem3  47203  dfafn5b  47787  fundcmpsurinjlem2  48037  upgrimwlklem1  48551  lincresunit2  49143  isofnALT  49694