Theorem fnmpti 6606

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 6602	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
5	2, 4	mpbi 229	1 ⊢ 𝐹 Fn 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2104  ∀wral 3062  Vcvv 3437   ↦ cmpt 5164   Fn wfn 6453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-fun 6460  df-fn 6461

This theorem is referenced by:  dmmpti  6607  fconst  6690  dffn5  6860  idref  7050  eufnfv  7137  offn  7578  caofinvl  7595  fo1st  7883  fo2nd  7884  reldm  7917  fimaproj  8007  mapsnf1o2  8713  unfilem2  9127  fidomdm  9144  pwfilemOLD  9161  noinfep  9466  ssttrcl  9521  ttrcltr  9522  ttrclselem2  9532  aceq3lem  9926  dfac4  9928  ackbij2lem2  10046  cfslb2n  10074  axcc2lem  10242  dmct  10330  konigthlem  10374  rankcf  10583  tskuni  10589  seqf1o  13814  ccatlen  14327  ccatlenOLD  14328  ccatvalfn  14335  swrdlen  14409  swrdwrdsymb  14424  swrdswrd  14467  sqrtf  15124  mptfzshft  15539  efcvgfsum  15844  prmreclem2  16667  1arith  16677  vdwlem6  16736  vdwlem8  16738  slotfn  16934  topnfn  17185  fnmre  17349  cidffn  17436  cidfn  17437  funcres  17660  initofn  17751  termofn  17752  zeroofn  17753  yonedainv  18048  fn0g  18396  smndex1igid  18592  smndex1n0mnd  18600  grpinvfn  18670  cycsubmel  18868  conjnmz  18917  psgnfn  19158  odf  19194  sylow1lem4  19255  pgpssslw  19268  sylow2blem3  19276  sylow3lem2  19282  cygctb  19542  dprd2da  19694  fnmgp  19771  rlmfn  20509  rrgsupp  20611  frlmup4  21057  asclfn  21134  evlslem1  21341  mdetrlin  21800  fncld  22222  hauseqlcld  22846  kqf  22947  filunirn  23082  fmf  23145  txflf  23206  clsnsg  23310  tgpconncomp  23313  qustgpopn  23320  qustgplem  23321  ustfn  23402  xmetunirn  23539  met1stc  23726  rrxmvallem  24617  ovolf  24695  vitali  24826  i1fmulc  24917  mbfi1fseqlem4  24932  itg2seq  24956  itg2monolem1  24964  i1fibl  25021  fncpn  25146  lhop1lem  25226  mdegxrf  25282  aannenlem3  25539  efabl  25755  logccv  25867  gausslemma2dlem1  26563  padicabvf  26828  mptelee  27312  wlkiswwlks2lem1  28283  clwlkclwwlklem2a2  28406  grpoinvf  28943  occllem  29714  pjfni  30112  pjmfn  30126  rnbra  30518  bra11  30519  kbass2  30528  hmopidmchi  30562  xppreima2  31037  abfmpunirn  31038  psgnfzto1stlem  31416  elrspunidl  31655  locfinreflem  31839  zarclsint  31871  zar0ring  31877  rhmpreimacn  31884  ofcfn  32117  sxbrsigalem3  32288  eulerpartgbij  32388  sseqfv1  32405  sseqfn  32406  sseqf  32408  sseqfv2  32410  signstlen  32595  msubrn  33540  msrf  33553  faclimlem1  33758  bj-evalfn  35293  bj-inftyexpitaufo  35421  matunitlindflem1  35821  poimirlem30  35855  mblfinlem2  35863  volsupnfl  35870  cnambfre  35873  itg2addnclem2  35877  itg2addnclem3  35878  ftc1anclem5  35902  ftc1anclem7  35904  sdclem2  35948  prdsbnd2  36001  rrncmslem  36038  diafn  39248  cdlemm10N  39332  dibfna  39368  lcfrlem9  39764  mapd1o  39862  hdmapfnN  40043  hgmapfnN  40102  evlsbagval  40470  fsuppind  40474  mhphf  40480  rmxypairf1o  40929  hbtlem6  41150  dgraaf  41168  cytpfn  41229  ntrf  41946  uzmptshftfval  42177  binomcxplemrat  42181  addrfn  42303  subrfn  42304  mulvfn  42305  limsup10exlem  43542  liminfvalxr  43553  fourierdlem62  43938  fourierdlem70  43946  fourierdlem71  43947  fmtnorn  45230  zrinitorngc  45802  zrtermorngc  45803  zrtermoringc  45872