Theorem fnmpti 6493

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  ∀wral 3140  Vcvv 3496   ↦ cmpt 5148   Fn wfn 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-fun 6359  df-fn 6360

This theorem is referenced by:  dmmpti  6494  fconst  6567  dffn5  6726  idref  6910  eufnfv  6993  offn  7422  caofinvl  7438  fo1st  7711  fo2nd  7712  reldm  7745  fimaproj  7831  mapsnf1o2  8460  unfilem2  8785  fidomdm  8803  pwfilem  8820  noinfep  9125  aceq3lem  9548  dfac4  9550  ackbij2lem2  9664  cfslb2n  9692  axcc2lem  9860  dmct  9948  konigthlem  9992  rankcf  10201  tskuni  10207  seqf1o  13414  ccatlen  13929  ccatlenOLD  13930  ccatvalfn  13937  swrdlen  14011  swrdwrdsymb  14026  swrdswrd  14069  sqrtf  14725  mptfzshft  15135  fprodrev  15333  efcvgfsum  15441  prmreclem2  16255  1arith  16265  vdwlem6  16324  vdwlem8  16326  slotfn  16503  topnfn  16701  fnmre  16864  cidffn  16951  cidfn  16952  funcres  17168  yonedainv  17533  fn0g  17875  smndex1igid  18071  smndex1n0mnd  18079  grpinvfn  18147  cycsubmel  18345  conjnmz  18394  psgnfn  18631  odf  18667  sylow1lem4  18728  pgpssslw  18741  sylow2blem3  18749  sylow3lem2  18755  cygctb  19014  dprd2da  19166  fnmgp  19243  rlmfn  19964  rrgsupp  20066  asclfn  20112  evlslem1  20297  frlmup4  20947  mdetrlin  21213  fncld  21632  hauseqlcld  22256  kqf  22357  filunirn  22492  fmf  22555  txflf  22616  clsnsg  22720  tgpconncomp  22723  qustgpopn  22730  qustgplem  22731  ustfn  22812  xmetunirn  22949  met1stc  23133  rrxmvallem  24009  ovolf  24085  vitali  24216  i1fmulc  24306  mbfi1fseqlem4  24321  itg2seq  24345  itg2monolem1  24353  i1fibl  24410  fncpn  24532  lhop1lem  24612  mdegxrf  24664  aannenlem3  24921  efabl  25136  logccv  25248  gausslemma2dlem1  25944  padicabvf  26209  mptelee  26683  wlkiswwlks2lem1  27649  clwlkclwwlklem2a2  27773  grpoinvf  28311  occllem  29082  pjfni  29480  pjmfn  29494  rnbra  29886  bra11  29887  kbass2  29896  hmopidmchi  29930  xppreima2  30397  abfmpunirn  30399  psgnfzto1stlem  30744  locfinreflem  31106  ofcfn  31361  sxbrsigalem3  31532  eulerpartgbij  31632  sseqfv1  31649  sseqfn  31650  sseqf  31652  sseqfv2  31654  signstlen  31839  msubrn  32778  msrf  32791  faclimlem1  32977  bj-evalfn  34367  bj-inftyexpitaufo  34486  matunitlindflem1  34890  poimirlem30  34924  mblfinlem2  34932  volsupnfl  34939  cnambfre  34942  itg2addnclem2  34946  itg2addnclem3  34947  ftc1anclem5  34973  ftc1anclem7  34975  sdclem2  35019  prdsbnd2  35075  rrncmslem  35112  diafn  38172  cdlemm10N  38256  dibfna  38292  lcfrlem9  38688  mapd1o  38786  hdmapfnN  38967  hgmapfnN  39026  rmxypairf1o  39515  hbtlem6  39736  dgraaf  39754  cytpfn  39815  ntrf  40480  uzmptshftfval  40685  binomcxplemrat  40689  addrfn  40811  subrfn  40812  mulvfn  40813  limsup10exlem  42060  liminfvalxr  42071  fourierdlem62  42460  fourierdlem70  42468  fourierdlem71  42469  fmtnorn  43703  zrinitorngc  44278  zrtermorngc  44279  zrtermoringc  44348