Theorem fnmpt 6705

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  ∀wral 3054  Vcvv 3472   ↦ cmpt 5239   Fn wfn 6553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-fun 6560  df-fn 6561

This theorem is referenced by:  fnmptd  6706  mpt0  6707  fnmptfvd  7059  ralrnmptw  7113  ralrnmpt  7115  fmpt  7129  fmpt2d  7143  f1ocnvd  7682  offval2  7715  ofrfval2  7716  mptcnfimad  8008  fsplitfpar  8140  mptelixpg  8972  fifo  9482  cantnflem1  9739  infmap2  10267  compssiso  10424  gruiun  10849  mptnn0fsupp  14028  mptnn0fsuppr  14030  seqof  14090  rlimi2  15537  prdsbas3  17517  prdsbascl  17519  prdsdsval2  17520  quslem  17579  fnmrc  17641  isofn  17812  ghmquskerco  19300  pmtrrn  19477  pmtrfrn  19478  pmtrdifwrdellem2  19502  gsummptcl  19987  mptscmfsupp0  20925  ofco2  22467  pmatcollpw2lem  22793  neif  23118  tgrest  23177  cmpfi  23426  elptr2  23592  xkoptsub  23672  ptcmplem2  24071  ptcmplem3  24072  prdsxmetlem  24388  prdsxmslem2  24552  bcth3  25373  uniioombllem6  25631  itg2const  25784  ellimc2  25920  dvrec  26001  dvmptres3  26002  ulmss  26449  ulmdvlem1  26452  ulmdvlem2  26453  ulmdvlem3  26454  itgulm2  26461  psercn  26479  tgjustr  28424  f1o3d  32570  f1od2  32660  psgnfzto1stlem  33007  frlmdim  33537  rmulccn  33781  esumnul  33919  esum0  33920  gsumesum  33930  ofcfval2  33975  signsplypnf  34434  signsply0  34435  hgt750lemb  34540  wevgblacfn  34983  matunitlindflem1  37364  matunitlindflem2  37365  cdlemk56  40717  dicfnN  40929  hbtlem7  42857  refsumcn  44700  wessf1ornlem  44862  choicefi  44877  axccdom  44899  fsumsermpt  45270  liminfval2  45459  stoweidlem31  45722  stoweidlem59  45750  stirlinglem13  45777  dirkercncflem2  45795  fourierdlem62  45859  subsaliuncllem  46048  subsaliuncl  46049  hoidmvlelem3  46288  dfafn5b  46844  fundcmpsurinjlem2  47041  lincresunit2  47942