Theorem fnmpti 6723

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 3071	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		fnmpti.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	mptfng 6719	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 230	1 ⊢ 𝐹 Fn 𝐴

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   ↦ cmpt 5249   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-fun 6575  df-fn 6576

This theorem is referenced by:  dmmpti  6724  fconst  6807  dffn5  6980  idref  7180  eufnfv  7266  offn  7727  caofinvl  7745  fo1st  8050  fo2nd  8051  reldm  8085  fimaproj  8176  mapsnf1o2  8952  unfilem2  9372  fidomdm  9402  pwfilemOLD  9416  noinfep  9729  ssttrcl  9784  ttrcltr  9785  ttrclselem2  9795  aceq3lem  10189  dfac4  10191  ackbij2lem2  10308  cfslb2n  10337  axcc2lem  10505  dmct  10593  konigthlem  10637  rankcf  10846  tskuni  10852  seqf1o  14094  ccatlen  14623  ccatvalfn  14629  swrdlen  14695  swrdwrdsymb  14710  swrdswrd  14753  sqrtf  15412  mptfzshft  15826  efcvgfsum  16134  prmreclem2  16964  1arith  16974  vdwlem6  17033  vdwlem8  17035  slotfn  17231  topnfn  17485  fnmre  17649  cidffn  17736  cidfn  17737  funcres  17960  initofn  18054  termofn  18055  zeroofn  18056  yonedainv  18351  fn0g  18701  smndex1igid  18939  smndex1n0mnd  18947  grpinvfn  19021  cycsubmel  19240  conjnmz  19292  ghmquskerco  19324  psgnfn  19543  odf  19579  sylow1lem4  19643  pgpssslw  19656  sylow2blem3  19664  sylow3lem2  19670  cygctb  19934  dprd2da  20086  fnmgp  20163  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  rrgsupp  20723  rlmfn  21220  frlmup4  21844  asclfn  21924  evlslem1  22129  psdmplcl  22189  psdadd  22190  psdmul  22193  mdetrlin  22629  fncld  23051  hauseqlcld  23675  kqf  23776  filunirn  23911  fmf  23974  txflf  24035  clsnsg  24139  tgpconncomp  24142  qustgpopn  24149  qustgplem  24150  ustfn  24231  xmetunirn  24368  met1stc  24555  rrxmvallem  25457  ovolf  25536  vitali  25667  i1fmulc  25758  mbfi1fseqlem4  25773  itg2seq  25797  itg2monolem1  25805  i1fibl  25863  fncpn  25989  lhop1lem  26072  mdegxrf  26127  aannenlem3  26390  efabl  26610  logccv  26723  gausslemma2dlem1  27428  padicabvf  27693  mptelee  28928  wlkiswwlks2lem1  29902  clwlkclwwlklem2a2  30025  grpoinvf  30564  occllem  31335  pjfni  31733  pjmfn  31747  rnbra  32139  bra11  32140  kbass2  32149  hmopidmchi  32183  xppreima2  32669  abfmpunirn  32670  psgnfzto1stlem  33093  elrspunidl  33421  locfinreflem  33786  zarclsint  33818  zar0ring  33824  rhmpreimacn  33831  ofcfn  34064  sxbrsigalem3  34237  eulerpartgbij  34337  sseqfv1  34354  sseqfn  34355  sseqf  34357  sseqfv2  34359  signstlen  34544  msubrn  35497  msrf  35510  faclimlem1  35705  weiunlem2  36429  bj-evalfn  37040  bj-inftyexpitaufo  37168  matunitlindflem1  37576  poimirlem30  37610  mblfinlem2  37618  volsupnfl  37625  cnambfre  37628  itg2addnclem2  37632  itg2addnclem3  37633  ftc1anclem5  37657  ftc1anclem7  37659  sdclem2  37702  prdsbnd2  37755  rrncmslem  37792  diafn  40991  cdlemm10N  41075  dibfna  41111  lcfrlem9  41507  mapd1o  41605  hdmapfnN  41786  hgmapfnN  41845  evlsvvval  42518  fsuppind  42545  rmxypairf1o  42868  hbtlem6  43086  dgraaf  43104  cytpfn  43162  tfsconcatrev  43310  ntrf  44085  uzmptshftfval  44315  binomcxplemrat  44319  addrfn  44441  subrfn  44442  mulvfn  44443  limsup10exlem  45693  liminfvalxr  45704  fourierdlem62  46089  fourierdlem70  46097  fourierdlem71  46098  fmtnorn  47408