Theorem fnmpti 6678

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ↦ cmpt 5192   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-fun 6538  df-fn 6539

This theorem is referenced by:  dmmpti  6679  fconst  6764  dffn5  6939  idref  7142  eufnfv  7227  offn  7687  caofinvl  7706  fo1st  8002  fo2nd  8003  reldm  8037  fimaproj  8127  mapsnf1o2  8888  unfilem2  9262  fidomdm  9287  noinfep  9625  ssttrcl  9680  ttrcltr  9681  ttrclselem2  9691  aceq3lem  10100  dfac4  10102  ackbij2lem2  10218  cfslb2n  10247  axcc2lem  10415  dmct  10503  konigthlem  10548  rankcf  10757  tskuni  10763  seqf1o  14075  ccatlen  14608  ccatvalfn  14614  swrdlen  14681  swrdwrdsymb  14696  swrdswrd  14738  sqrtf  15411  mptfzshft  15825  efcvgfsum  16135  prmreclem2  16972  1arith  16982  vdwlem6  17041  vdwlem8  17043  slotfn  17239  topnfn  17473  fnmre  17638  cidffn  17729  cidfn  17730  funcres  17948  initofn  18039  termofn  18040  zeroofn  18041  yonedainv  18332  fn0g  18716  smndex1igid  18960  smndex1igidOLD  18961  smndex1n0mnd  18969  grpinvfn  19043  cycsubmel  19266  conjnmz  19317  ghmquskerco  19349  psgnfn  19566  odf  19602  sylow1lem4  19666  pgpssslw  19679  sylow2blem3  19687  sylow3lem2  19693  cygctb  19957  dprd2da  20109  fnmgp  20213  zrinitorngc  20741  zrtermorngc  20742  zrtermoringc  20774  rrgsupp  20800  rlmfn  21311  frlmup4  21951  asclfn  22030  evlslem1  22233  evlsvvval  22244  psdmplcl  22325  psdadd  22326  psdmul  22329  psdmvr  22332  mdetrlin  22759  fncld  23179  hauseqlcld  23803  kqf  23904  filunirn  24039  fmf  24102  txflf  24163  clsnsg  24267  tgpconncomp  24270  qustgpopn  24277  qustgplem  24278  ustfn  24359  xmetunirn  24494  met1stc  24678  rrxmvallem  25563  ovolf  25641  vitali  25772  i1fmulc  25862  mbfi1fseqlem4  25877  itg2seq  25901  itg2monolem1  25909  i1fibl  25967  fncpn  26092  lhop1lem  26172  mdegxrf  26225  aannenlem3  26493  efabl  26715  logccv  26828  gausslemma2dlem1  27530  padicabvf  27795  mpteleeOLD  29245  wlkiswwlks2lem1  30218  clwlkclwwlklem2a2  30344  grpoinvf  30884  occllem  31655  pjfni  32053  pjmfn  32067  rnbra  32459  bra11  32460  kbass2  32469  hmopidmchi  32503  xppreima2  32996  abfmpunirn  32997  psgnfzto1stlem  33420  elrspunidl  33736  locfinreflem  34230  zarclsint  34262  zar0ring  34268  rhmpreimacn  34275  ofcfn  34490  sxbrsigalem3  34662  eulerpartgbij  34762  sseqfv1  34779  sseqfn  34780  sseqf  34782  sseqfv2  34784  signstlen  34954  kardfn  35564  vonf1oonfo  35599  msubrn  36021  msrf  36034  faclimlem1  36235  weiunlem  36994  bj-evalfn  37735  bj-inftyexpitaufo  37866  matunitlindflem1  38287  poimirlem30  38321  mblfinlem2  38329  volsupnfl  38336  cnambfre  38339  itg2addnclem2  38343  itg2addnclem3  38344  ftc1anclem5  38368  ftc1anclem7  38370  sdclem2  38413  prdsbnd2  38466  rrncmslem  38503  diafn  41828  cdlemm10N  41912  dibfna  41948  lcfrlem9  42344  mapd1o  42442  hdmapfnN  42623  hgmapfnN  42682  fsuppind  43342  rmxypairf1o  43658  hbtlem6  43876  dgraaf  43894  cytpfn  43948  tfsconcatrev  44095  ntrf  44869  uzmptshftfval  45076  binomcxplemrat  45080  addrfn  45200  subrfn  45201  mulvfn  45202  limsup10exlem  46506  liminfvalxr  46517  fourierdlem62  46902  fourierdlem70  46910  fourierdlem71  46911  cjnpoly  47646  fmtnorn  48306  tposideq  49686  cicfn  49840  fucofn22  50138  fucoid  50146  dfinito4  50299  crosspalti  50667