Theorem fnmpti 6711

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   ↦ cmpt 5225   Fn wfn 6556

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-fun 6563  df-fn 6564

This theorem is referenced by:  dmmpti  6712  fconst  6794  dffn5  6967  idref  7166  eufnfv  7249  offn  7710  caofinvl  7729  fo1st  8034  fo2nd  8035  reldm  8069  fimaproj  8160  mapsnf1o2  8934  unfilem2  9344  fidomdm  9374  noinfep  9700  ssttrcl  9755  ttrcltr  9756  ttrclselem2  9766  aceq3lem  10160  dfac4  10162  ackbij2lem2  10279  cfslb2n  10308  axcc2lem  10476  dmct  10564  konigthlem  10608  rankcf  10817  tskuni  10823  seqf1o  14084  ccatlen  14613  ccatvalfn  14619  swrdlen  14685  swrdwrdsymb  14700  swrdswrd  14743  sqrtf  15402  mptfzshft  15814  efcvgfsum  16122  prmreclem2  16955  1arith  16965  vdwlem6  17024  vdwlem8  17026  slotfn  17221  topnfn  17470  fnmre  17634  cidffn  17721  cidfn  17722  funcres  17941  initofn  18032  termofn  18033  zeroofn  18034  yonedainv  18326  fn0g  18676  smndex1igid  18917  smndex1n0mnd  18925  grpinvfn  18999  cycsubmel  19218  conjnmz  19270  ghmquskerco  19302  psgnfn  19519  odf  19555  sylow1lem4  19619  pgpssslw  19632  sylow2blem3  19640  sylow3lem2  19646  cygctb  19910  dprd2da  20062  fnmgp  20139  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  rrgsupp  20701  rlmfn  21197  frlmup4  21821  asclfn  21901  evlslem1  22106  psdmplcl  22166  psdadd  22167  psdmul  22170  psdmvr  22173  mdetrlin  22608  fncld  23030  hauseqlcld  23654  kqf  23755  filunirn  23890  fmf  23953  txflf  24014  clsnsg  24118  tgpconncomp  24121  qustgpopn  24128  qustgplem  24129  ustfn  24210  xmetunirn  24347  met1stc  24534  rrxmvallem  25438  ovolf  25517  vitali  25648  i1fmulc  25738  mbfi1fseqlem4  25753  itg2seq  25777  itg2monolem1  25785  i1fibl  25843  fncpn  25969  lhop1lem  26052  mdegxrf  26107  aannenlem3  26372  efabl  26592  logccv  26705  gausslemma2dlem1  27410  padicabvf  27675  mptelee  28910  wlkiswwlks2lem1  29889  clwlkclwwlklem2a2  30012  grpoinvf  30551  occllem  31322  pjfni  31720  pjmfn  31734  rnbra  32126  bra11  32127  kbass2  32136  hmopidmchi  32170  xppreima2  32661  abfmpunirn  32662  psgnfzto1stlem  33120  elrspunidl  33456  locfinreflem  33839  zarclsint  33871  zar0ring  33877  rhmpreimacn  33884  ofcfn  34101  sxbrsigalem3  34274  eulerpartgbij  34374  sseqfv1  34391  sseqfn  34392  sseqf  34394  sseqfv2  34396  signstlen  34582  msubrn  35534  msrf  35547  faclimlem1  35743  weiunlem2  36464  bj-evalfn  37075  bj-inftyexpitaufo  37203  matunitlindflem1  37623  poimirlem30  37657  mblfinlem2  37665  volsupnfl  37672  cnambfre  37675  itg2addnclem2  37679  itg2addnclem3  37680  ftc1anclem5  37704  ftc1anclem7  37706  sdclem2  37749  prdsbnd2  37802  rrncmslem  37839  diafn  41036  cdlemm10N  41120  dibfna  41156  lcfrlem9  41552  mapd1o  41650  hdmapfnN  41831  hgmapfnN  41890  evlsvvval  42573  fsuppind  42600  rmxypairf1o  42923  hbtlem6  43141  dgraaf  43159  cytpfn  43213  tfsconcatrev  43361  ntrf  44136  uzmptshftfval  44365  binomcxplemrat  44369  addrfn  44491  subrfn  44492  mulvfn  44493  limsup10exlem  45787  liminfvalxr  45798  fourierdlem62  46183  fourierdlem70  46191  fourierdlem71  46192  fmtnorn  47521  tposideq  48788  fucofn22  49035  fucoid  49043