Theorem fnmpti 6664

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  ∀wral 3076  Vcvv 3454   ↦ cmpt 5181   Fn wfn 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-fun 6523  df-fn 6524

This theorem is referenced by:  dmmpti  6665  fconst  6750  dffn5  6925  idref  7128  eufnfv  7213  offn  7673  caofinvl  7692  fo1st  7990  fo2nd  7991  reldm  8025  fimaproj  8115  mapsnf1o2  8876  unfilem2  9250  fidomdm  9277  noinfep  9615  ssttrcl  9670  ttrcltr  9671  ttrclselem2  9681  aceq3lem  10076  dfac4  10078  ackbij2lem2  10195  cfslb2n  10225  axcc2lem  10393  dmct  10481  konigthlem  10526  rankcf  10735  tskuni  10741  seqf1o  14056  ccatlen  14588  ccatvalfn  14594  swrdlen  14661  swrdwrdsymb  14676  swrdswrd  14718  sqrtf  15391  mptfzshft  15805  efcvgfsum  16116  prmreclem2  16953  1arith  16963  vdwlem6  17022  vdwlem8  17024  slotfn  17220  topnfn  17454  fnmre  17619  cidffn  17710  cidfn  17711  funcres  17929  initofn  18020  termofn  18021  zeroofn  18022  yonedainv  18313  fn0g  18697  smndex1igid  18940  smndex1igidOLD  18941  smndex1n0mnd  18949  grpinvfn  19023  cycsubmel  19241  conjnmz  19292  ghmquskerco  19324  psgnfn  19541  odf  19577  sylow1lem4  19641  pgpssslw  19654  sylow2blem3  19662  sylow3lem2  19668  cygctb  19932  dprd2da  20084  fnmgp  20188  zrinitorngc  20692  zrtermorngc  20693  zrtermoringc  20725  rrgsupp  20751  rlmfn  21257  frlmup4  21853  asclfn  21932  evlslem1  22135  evlsvvval  22146  psdmplcl  22227  psdadd  22228  psdmul  22231  psdmvr  22234  mdetrlin  22662  fncld  23082  hauseqlcld  23706  kqf  23807  filunirn  23942  fmf  24005  txflf  24066  clsnsg  24170  tgpconncomp  24173  qustgpopn  24180  qustgplem  24181  ustfn  24262  xmetunirn  24397  met1stc  24581  rrxmvallem  25466  ovolf  25544  vitali  25675  i1fmulc  25765  mbfi1fseqlem4  25780  itg2seq  25804  itg2monolem1  25812  i1fibl  25870  fncpn  25995  lhop1lem  26075  mdegxrf  26128  aannenlem3  26394  efabl  26615  logccv  26728  gausslemma2dlem1  27430  padicabvf  27695  mpteleeOLD  29096  wlkiswwlks2lem1  30069  clwlkclwwlklem2a2  30195  grpoinvf  30735  occllem  31506  pjfni  31904  pjmfn  31918  rnbra  32310  bra11  32311  kbass2  32320  hmopidmchi  32354  xppreima2  32853  abfmpunirn  32854  psgnfzto1stlem  33280  elrspunidl  33614  locfinreflem  34137  zarclsint  34169  zar0ring  34175  rhmpreimacn  34182  ofcfn  34397  sxbrsigalem3  34569  eulerpartgbij  34669  sseqfv1  34686  sseqfn  34687  sseqf  34689  sseqfv2  34691  signstlen  34861  vonf1oonfo  35458  msubrn  35879  msrf  35892  faclimlem1  36093  weiunlem  36823  bj-evalfn  37563  bj-inftyexpitaufo  37694  matunitlindflem1  38115  poimirlem30  38149  mblfinlem2  38157  volsupnfl  38164  cnambfre  38167  itg2addnclem2  38171  itg2addnclem3  38172  ftc1anclem5  38196  ftc1anclem7  38198  sdclem2  38241  prdsbnd2  38294  rrncmslem  38331  diafn  41658  cdlemm10N  41742  dibfna  41778  lcfrlem9  42174  mapd1o  42272  hdmapfnN  42453  hgmapfnN  42512  fsuppind  43172  rmxypairf1o  43488  hbtlem6  43706  dgraaf  43724  cytpfn  43778  tfsconcatrev  43925  ntrf  44699  uzmptshftfval  44922  binomcxplemrat  44926  addrfn  45047  subrfn  45048  mulvfn  45049  limsup10exlem  46346  liminfvalxr  46357  fourierdlem62  46742  fourierdlem70  46750  fourierdlem71  46751  nthrucw  47462  cjnpoly  47483  fmtnorn  48143  tposideq  49509  cicfn  49663  fucofn22  49961  fucoid  49969  dfinito4  50122