Theorem fnmpti 6686

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3052  Vcvv 3464   ↦ cmpt 5206   Fn wfn 6531

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6538  df-fn 6539

This theorem is referenced by:  dmmpti  6687  fconst  6769  dffn5  6942  idref  7141  eufnfv  7226  offn  7689  caofinvl  7708  fo1st  8013  fo2nd  8014  reldm  8048  fimaproj  8139  mapsnf1o2  8913  unfilem2  9321  fidomdm  9351  noinfep  9679  ssttrcl  9734  ttrcltr  9735  ttrclselem2  9745  aceq3lem  10139  dfac4  10141  ackbij2lem2  10258  cfslb2n  10287  axcc2lem  10455  dmct  10543  konigthlem  10587  rankcf  10796  tskuni  10802  seqf1o  14066  ccatlen  14598  ccatvalfn  14604  swrdlen  14670  swrdwrdsymb  14685  swrdswrd  14728  sqrtf  15387  mptfzshft  15799  efcvgfsum  16107  prmreclem2  16942  1arith  16952  vdwlem6  17011  vdwlem8  17013  slotfn  17208  topnfn  17444  fnmre  17608  cidffn  17695  cidfn  17696  funcres  17914  initofn  18005  termofn  18006  zeroofn  18007  yonedainv  18298  fn0g  18646  smndex1igid  18887  smndex1n0mnd  18895  grpinvfn  18969  cycsubmel  19188  conjnmz  19240  ghmquskerco  19272  psgnfn  19487  odf  19523  sylow1lem4  19587  pgpssslw  19600  sylow2blem3  19608  sylow3lem2  19614  cygctb  19878  dprd2da  20030  fnmgp  20107  zrinitorngc  20607  zrtermorngc  20608  zrtermoringc  20640  rrgsupp  20666  rlmfn  21153  frlmup4  21766  asclfn  21846  evlslem1  22045  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  mdetrlin  22545  fncld  22965  hauseqlcld  23589  kqf  23690  filunirn  23825  fmf  23888  txflf  23949  clsnsg  24053  tgpconncomp  24056  qustgpopn  24063  qustgplem  24064  ustfn  24145  xmetunirn  24281  met1stc  24465  rrxmvallem  25361  ovolf  25440  vitali  25571  i1fmulc  25661  mbfi1fseqlem4  25676  itg2seq  25700  itg2monolem1  25708  i1fibl  25766  fncpn  25892  lhop1lem  25975  mdegxrf  26030  aannenlem3  26295  efabl  26516  logccv  26629  gausslemma2dlem1  27334  padicabvf  27599  mptelee  28879  wlkiswwlks2lem1  29856  clwlkclwwlklem2a2  29979  grpoinvf  30518  occllem  31289  pjfni  31687  pjmfn  31701  rnbra  32093  bra11  32094  kbass2  32103  hmopidmchi  32137  xppreima2  32634  abfmpunirn  32635  psgnfzto1stlem  33116  elrspunidl  33448  locfinreflem  33876  zarclsint  33908  zar0ring  33914  rhmpreimacn  33921  ofcfn  34136  sxbrsigalem3  34309  eulerpartgbij  34409  sseqfv1  34426  sseqfn  34427  sseqf  34429  sseqfv2  34431  signstlen  34604  msubrn  35556  msrf  35569  faclimlem1  35765  weiunlem2  36486  bj-evalfn  37097  bj-inftyexpitaufo  37225  matunitlindflem1  37645  poimirlem30  37679  mblfinlem2  37687  volsupnfl  37694  cnambfre  37697  itg2addnclem2  37701  itg2addnclem3  37702  ftc1anclem5  37726  ftc1anclem7  37728  sdclem2  37771  prdsbnd2  37824  rrncmslem  37861  diafn  41058  cdlemm10N  41142  dibfna  41178  lcfrlem9  41574  mapd1o  41672  hdmapfnN  41853  hgmapfnN  41912  evlsvvval  42561  fsuppind  42588  rmxypairf1o  42910  hbtlem6  43128  dgraaf  43146  cytpfn  43200  tfsconcatrev  43347  ntrf  44122  uzmptshftfval  44345  binomcxplemrat  44349  addrfn  44471  subrfn  44472  mulvfn  44473  limsup10exlem  45781  liminfvalxr  45792  fourierdlem62  46177  fourierdlem70  46185  fourierdlem71  46186  fmtnorn  47528  tposideq  48843  cicfn  48989  fucofn22  49231  fucoid  49239  dfinito4  49366