Theorem fnmpti 6682

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fnmpti.1	⊢ 𝐵 ∈ V
fnmpti.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fnmpti	⊢ 𝐹 Fn 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fnmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3 ⊢ 𝐵 ∈ V
2	1	rgenw 3081	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6678	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 233	1 ⊢ 𝐹 Fn 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3077  Vcvv 3451   ↦ cmpt 5186   Fn wfn 6533

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6540  df-fn 6541

This theorem is used by:  dmmpti  6683  fconst  6768  dffn5  6943  idref  7149  eufnfv  7235  offn  7706  caofinvl  7725  fo1st  8021  fo2nd  8022  reldm  8055  fimaproj  8152  mapsnf1o2  8922  unfilem2  9298  fidomdm  9323  noinfep  9661  ssttrcl  9716  ttrcltr  9717  ttrclselem2  9727  aceq3lem  10199  dfac4  10201  ackbij2lem2  10317  cfslb2n  10346  axcc2lem  10514  dmct  10602  dmctOLD  10603  konigthlem  10653  rankcf  10862  tskuni  10868  seqf1o  14186  ccatlen  14720  ccatvalfn  14726  swrdlen  14795  swrdwrdsymb  14812  swrdswrd  14854  sqrtf  15531  mptfzshft  15944  efcvgfsum  16252  prmreclem2  17095  1arith  17105  vdwlem6  17164  vdwlem8  17166  slotfn  17362  topnfn  17596  fnmre  17761  cidffn  17852  cidfn  17853  funcres  18071  initofn  18162  termofn  18163  zeroofn  18164  yonedainv  18455  fn0g  18843  smndex1igid  19102  smndex1igidOLD  19103  smndex1n0mnd  19111  grpinvfn  19192  cycsubmel  19415  conjnmz  19466  ghmquskerco  19498  psgnfn  19715  odf  19751  sylow1lem4  19815  pgpssslw  19828  sylow2blem3  19836  sylow3lem2  19842  cygctb  20106  dprd2da  20258  fnmgp  20362  zrinitorngc  20894  zrtermorngc  20895  zrtermoringc  20927  rrgsupp  20953  rlmfn  21465  frlmup4  22107  asclfn  22188  evlslem1  22391  evlsvvval  22402  psdmplcl  22483  psdadd  22484  psdmul  22487  psdmvr  22490  mdetrlin  22917  matunitlindflem1  22994  fncld  23340  hauseqlcld  23965  kqf  24066  filunirn  24201  fmf  24264  txflf  24325  clsnsg  24429  tgpconncomp  24432  qustgpopn  24439  qustgplem  24440  ustfn  24521  xmetunirn  24656  met1stc  24840  rrxmvallem  25725  ovolf  25803  vitali  25934  i1fmulc  26024  mbfi1fseqlem4  26039  itg2seq  26063  itg2monolem1  26071  i1fibl  26128  fncpn  26253  lhop1lem  26333  mdegxrf  26386  aannenlem3  26657  efabl  26878  logccv  26991  gausslemma2dlem1  27693  padicabvf  27958  mpteleeOLD  29473  wlkiswwlks2lem1  30458  clwlkclwwlklem2a2  30584  grpoinvf  31134  occllem  31905  pjfni  32303  pjmfn  32317  rnbra  32709  bra11  32710  kbass2  32719  hmopidmchi  32753  xppreima2  33245  abfmpunirn  33246  psgnfzto1stlem  33661  elrspunidl  33978  locfinreflem  34472  zarclsint  34504  zar0ring  34510  rhmpreimacn  34517  ofcfn  34732  sxbrsigalem3  34904  eulerpartgbij  35004  sseqfv1  35021  sseqfn  35022  sseqf  35024  sseqfv2  35026  signstlen  35196  kardfn  35819  vonf1oonfo  35898  msubrn  36294  msrf  36307  faclimlem1  36508  weiunlem  37251  bj-evalfn  37994  bj-inftyexpitaufo  38123  poimirlem30  38568  mblfinlem2  38576  volsupnfl  38583  cnambfre  38586  itg2addnclem2  38590  itg2addnclem3  38591  ftc1anclem5  38615  ftc1anclem7  38617  sdclem2  38676  prdsbnd2  38729  rrncmslem  38766  diafn  42091  cdlemm10N  42175  dibfna  42211  lcfrlem9  42607  mapd1o  42705  hdmapfnN  42886  hgmapfnN  42945  fsuppind  43618  rmxypairf1o  43917  hbtlem6  44130  dgraaf  44148  cytpfn  44202  tfsconcatrev  44349  ntrf  45122  uzmptshftfval  45329  binomcxplemrat  45333  addrfn  45453  subrfn  45454  mulvfn  45455  limsup10exlem  46781  liminfvalxr  46792  fourierdlem62  47177  fourierdlem70  47185  fourierdlem71  47186  cjnpoly  47938  fmtnorn  48618  tposideq  49995  cicfn  50149  fucofn22  50447  fucoid  50455  dfinito4  50608  crosspaltd  50965  crossp3d  50966  veronesevrowd  50978  veronesematrowd  50980  veroquadmodzerod  50983