Theorem fnmpti 6691

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

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

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 5299  ax-nul 5306  ax-pr 5427

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-fun 6543  df-fn 6544

This theorem is referenced by:  dmmpti  6692  fconst  6775  dffn5  6948  idref  7141  eufnfv  7228  offn  7680  caofinvl  7697  fo1st  7992  fo2nd  7993  reldm  8027  fimaproj  8118  mapsnf1o2  8885  unfilem2  9308  fidomdm  9326  pwfilemOLD  9343  noinfep  9652  ssttrcl  9707  ttrcltr  9708  ttrclselem2  9718  aceq3lem  10112  dfac4  10114  ackbij2lem2  10232  cfslb2n  10260  axcc2lem  10428  dmct  10516  konigthlem  10560  rankcf  10769  tskuni  10775  seqf1o  14006  ccatlen  14522  ccatvalfn  14528  swrdlen  14594  swrdwrdsymb  14609  swrdswrd  14652  sqrtf  15307  mptfzshft  15721  efcvgfsum  16026  prmreclem2  16847  1arith  16857  vdwlem6  16916  vdwlem8  16918  slotfn  17114  topnfn  17368  fnmre  17532  cidffn  17619  cidfn  17620  funcres  17843  initofn  17934  termofn  17935  zeroofn  17936  yonedainv  18231  fn0g  18579  smndex1igid  18782  smndex1n0mnd  18790  grpinvfn  18863  cycsubmel  19072  conjnmz  19121  psgnfn  19364  odf  19400  sylow1lem4  19464  pgpssslw  19477  sylow2blem3  19485  sylow3lem2  19491  cygctb  19755  dprd2da  19907  fnmgp  19984  rlmfn  20805  rrgsupp  20900  frlmup4  21348  asclfn  21427  evlslem1  21637  mdetrlin  22096  fncld  22518  hauseqlcld  23142  kqf  23243  filunirn  23378  fmf  23441  txflf  23502  clsnsg  23606  tgpconncomp  23609  qustgpopn  23616  qustgplem  23617  ustfn  23698  xmetunirn  23835  met1stc  24022  rrxmvallem  24913  ovolf  24991  vitali  25122  i1fmulc  25213  mbfi1fseqlem4  25228  itg2seq  25252  itg2monolem1  25260  i1fibl  25317  fncpn  25442  lhop1lem  25522  mdegxrf  25578  aannenlem3  25835  efabl  26051  logccv  26163  gausslemma2dlem1  26859  padicabvf  27124  mptelee  28143  wlkiswwlks2lem1  29113  clwlkclwwlklem2a2  29236  grpoinvf  29773  occllem  30544  pjfni  30942  pjmfn  30956  rnbra  31348  bra11  31349  kbass2  31358  hmopidmchi  31392  xppreima2  31864  abfmpunirn  31865  psgnfzto1stlem  32247  ghmquskerco  32518  elrspunidl  32535  locfinreflem  32809  zarclsint  32841  zar0ring  32847  rhmpreimacn  32854  ofcfn  33087  sxbrsigalem3  33260  eulerpartgbij  33360  sseqfv1  33377  sseqfn  33378  sseqf  33380  sseqfv2  33382  signstlen  33567  msubrn  34509  msrf  34522  faclimlem1  34702  bj-evalfn  35944  bj-inftyexpitaufo  36072  matunitlindflem1  36473  poimirlem30  36507  mblfinlem2  36515  volsupnfl  36522  cnambfre  36525  itg2addnclem2  36529  itg2addnclem3  36530  ftc1anclem5  36554  ftc1anclem7  36556  sdclem2  36599  prdsbnd2  36652  rrncmslem  36689  diafn  39894  cdlemm10N  39978  dibfna  40014  lcfrlem9  40410  mapd1o  40508  hdmapfnN  40689  hgmapfnN  40748  evlsvvval  41133  fsuppind  41160  rmxypairf1o  41636  hbtlem6  41857  dgraaf  41875  cytpfn  41936  tfsconcatrev  42084  ntrf  42860  uzmptshftfval  43091  binomcxplemrat  43095  addrfn  43217  subrfn  43218  mulvfn  43219  limsup10exlem  44475  liminfvalxr  44486  fourierdlem62  44871  fourierdlem70  44879  fourierdlem71  44880  fmtnorn  46189  zrinitorngc  46852  zrtermorngc  46853  zrtermoringc  46922