Theorem fnmpti 6689

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ↦ cmpt 5229   Fn wfn 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5297  ax-nul 5304  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-fun 6541  df-fn 6542

This theorem is referenced by:  dmmpti  6690  fconst  6773  dffn5  6946  idref  7138  eufnfv  7225  offn  7677  caofinvl  7694  fo1st  7989  fo2nd  7990  reldm  8024  fimaproj  8115  mapsnf1o2  8883  unfilem2  9306  fidomdm  9324  pwfilemOLD  9341  noinfep  9650  ssttrcl  9705  ttrcltr  9706  ttrclselem2  9716  aceq3lem  10110  dfac4  10112  ackbij2lem2  10230  cfslb2n  10258  axcc2lem  10426  dmct  10514  konigthlem  10558  rankcf  10767  tskuni  10773  seqf1o  14004  ccatlen  14520  ccatvalfn  14526  swrdlen  14592  swrdwrdsymb  14607  swrdswrd  14650  sqrtf  15305  mptfzshft  15719  efcvgfsum  16024  prmreclem2  16845  1arith  16855  vdwlem6  16914  vdwlem8  16916  slotfn  17112  topnfn  17366  fnmre  17530  cidffn  17617  cidfn  17618  funcres  17841  initofn  17932  termofn  17933  zeroofn  17934  yonedainv  18229  fn0g  18577  smndex1igid  18780  smndex1n0mnd  18788  grpinvfn  18861  cycsubmel  19070  conjnmz  19119  psgnfn  19361  odf  19397  sylow1lem4  19461  pgpssslw  19474  sylow2blem3  19482  sylow3lem2  19488  cygctb  19751  dprd2da  19903  fnmgp  19980  rlmfn  20798  rrgsupp  20893  frlmup4  21339  asclfn  21416  evlslem1  21626  mdetrlin  22085  fncld  22507  hauseqlcld  23131  kqf  23232  filunirn  23367  fmf  23430  txflf  23491  clsnsg  23595  tgpconncomp  23598  qustgpopn  23605  qustgplem  23606  ustfn  23687  xmetunirn  23824  met1stc  24011  rrxmvallem  24902  ovolf  24980  vitali  25111  i1fmulc  25202  mbfi1fseqlem4  25217  itg2seq  25241  itg2monolem1  25249  i1fibl  25306  fncpn  25431  lhop1lem  25511  mdegxrf  25567  aannenlem3  25824  efabl  26040  logccv  26152  gausslemma2dlem1  26848  padicabvf  27113  mptelee  28132  wlkiswwlks2lem1  29102  clwlkclwwlklem2a2  29225  grpoinvf  29762  occllem  30533  pjfni  30931  pjmfn  30945  rnbra  31337  bra11  31338  kbass2  31347  hmopidmchi  31381  xppreima2  31853  abfmpunirn  31854  psgnfzto1stlem  32236  ghmquskerco  32491  elrspunidl  32503  locfinreflem  32757  zarclsint  32789  zar0ring  32795  rhmpreimacn  32802  ofcfn  33035  sxbrsigalem3  33208  eulerpartgbij  33308  sseqfv1  33325  sseqfn  33326  sseqf  33328  sseqfv2  33330  signstlen  33515  msubrn  34457  msrf  34470  faclimlem1  34650  bj-evalfn  35892  bj-inftyexpitaufo  36020  matunitlindflem1  36421  poimirlem30  36455  mblfinlem2  36463  volsupnfl  36470  cnambfre  36473  itg2addnclem2  36477  itg2addnclem3  36478  ftc1anclem5  36502  ftc1anclem7  36504  sdclem2  36547  prdsbnd2  36600  rrncmslem  36637  diafn  39842  cdlemm10N  39926  dibfna  39962  lcfrlem9  40358  mapd1o  40456  hdmapfnN  40637  hgmapfnN  40696  evlsvvval  41084  fsuppind  41111  rmxypairf1o  41582  hbtlem6  41803  dgraaf  41821  cytpfn  41882  tfsconcatrev  42030  ntrf  42806  uzmptshftfval  43037  binomcxplemrat  43041  addrfn  43163  subrfn  43164  mulvfn  43165  limsup10exlem  44422  liminfvalxr  44433  fourierdlem62  44818  fourierdlem70  44826  fourierdlem71  44827  fmtnorn  46136  zrinitorngc  46799  zrtermorngc  46800  zrtermoringc  46869