Theorem fnmpti 6628

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∀wral 3053  Vcvv 3431   ↦ cmpt 5153   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-fun 6487  df-fn 6488

This theorem is referenced by:  dmmpti  6629  fconst  6713  dffn5  6885  idref  7088  eufnfv  7173  offn  7633  caofinvl  7652  fo1st  7951  fo2nd  7952  reldm  7986  fimaproj  8075  mapsnf1o2  8832  unfilem2  9206  fidomdm  9234  noinfep  9572  ssttrcl  9627  ttrcltr  9628  ttrclselem2  9638  aceq3lem  10033  dfac4  10035  ackbij2lem2  10152  cfslb2n  10181  axcc2lem  10349  dmct  10437  konigthlem  10482  rankcf  10691  tskuni  10697  seqf1o  13996  ccatlen  14528  ccatvalfn  14534  swrdlen  14601  swrdwrdsymb  14616  swrdswrd  14658  sqrtf  15317  mptfzshft  15731  efcvgfsum  16042  prmreclem2  16879  1arith  16889  vdwlem6  16948  vdwlem8  16950  slotfn  17145  topnfn  17379  fnmre  17544  cidffn  17635  cidfn  17636  funcres  17854  initofn  17945  termofn  17946  zeroofn  17947  yonedainv  18238  fn0g  18622  smndex1igid  18865  smndex1igidOLD  18866  smndex1n0mnd  18874  grpinvfn  18948  cycsubmel  19166  conjnmz  19218  ghmquskerco  19250  psgnfn  19467  odf  19503  sylow1lem4  19567  pgpssslw  19580  sylow2blem3  19588  sylow3lem2  19594  cygctb  19858  dprd2da  20010  fnmgp  20114  zrinitorngc  20614  zrtermorngc  20615  zrtermoringc  20647  rrgsupp  20673  rlmfn  21180  frlmup4  21776  asclfn  21855  evlslem1  22058  evlsvvval  22069  psdmplcl  22150  psdadd  22151  psdmul  22154  psdmvr  22157  mdetrlin  22585  fncld  23005  hauseqlcld  23629  kqf  23730  filunirn  23865  fmf  23928  txflf  23989  clsnsg  24093  tgpconncomp  24096  qustgpopn  24103  qustgplem  24104  ustfn  24185  xmetunirn  24320  met1stc  24504  rrxmvallem  25389  ovolf  25467  vitali  25598  i1fmulc  25688  mbfi1fseqlem4  25703  itg2seq  25727  itg2monolem1  25735  i1fibl  25793  fncpn  25918  lhop1lem  25998  mdegxrf  26051  aannenlem3  26314  efabl  26532  logccv  26645  gausslemma2dlem1  27347  padicabvf  27612  mpteleeOLD  28982  wlkiswwlks2lem1  29955  clwlkclwwlklem2a2  30081  grpoinvf  30621  occllem  31392  pjfni  31790  pjmfn  31804  rnbra  32196  bra11  32197  kbass2  32206  hmopidmchi  32240  xppreima2  32743  abfmpunirn  32744  psgnfzto1stlem  33181  elrspunidl  33511  locfinreflem  34024  zarclsint  34056  zar0ring  34062  rhmpreimacn  34069  ofcfn  34284  sxbrsigalem3  34456  eulerpartgbij  34556  sseqfv1  34573  sseqfn  34574  sseqf  34576  sseqfv2  34578  signstlen  34751  msubrn  35757  msrf  35770  faclimlem1  35971  weiunlem  36691  bj-evalfn  37431  bj-inftyexpitaufo  37562  matunitlindflem1  37983  poimirlem30  38017  mblfinlem2  38025  volsupnfl  38032  cnambfre  38035  itg2addnclem2  38039  itg2addnclem3  38040  ftc1anclem5  38064  ftc1anclem7  38066  sdclem2  38109  prdsbnd2  38162  rrncmslem  38199  diafn  41526  cdlemm10N  41610  dibfna  41646  lcfrlem9  42042  mapd1o  42140  hdmapfnN  42321  hgmapfnN  42380  fsuppind  43040  rmxypairf1o  43356  hbtlem6  43574  dgraaf  43592  cytpfn  43646  tfsconcatrev  43793  ntrf  44567  uzmptshftfval  44790  binomcxplemrat  44794  addrfn  44915  subrfn  44916  mulvfn  44917  limsup10exlem  46215  liminfvalxr  46226  fourierdlem62  46611  fourierdlem70  46619  fourierdlem71  46620  nthrucw  47331  cjnpoly  47352  fmtnorn  48012  tposideq  49378  cicfn  49532  fucofn22  49830  fucoid  49838  dfinito4  49991