Theorem fnmpti 6693

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  ∀wral 3061  Vcvv 3474   ↦ cmpt 5231   Fn wfn 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  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 6545  df-fn 6546

This theorem is referenced by:  dmmpti  6694  fconst  6777  dffn5  6950  idref  7146  eufnfv  7233  offn  7685  caofinvl  7702  fo1st  7997  fo2nd  7998  reldm  8032  fimaproj  8123  mapsnf1o2  8890  unfilem2  9313  fidomdm  9331  pwfilemOLD  9348  noinfep  9657  ssttrcl  9712  ttrcltr  9713  ttrclselem2  9723  aceq3lem  10117  dfac4  10119  ackbij2lem2  10237  cfslb2n  10265  axcc2lem  10433  dmct  10521  konigthlem  10565  rankcf  10774  tskuni  10780  seqf1o  14013  ccatlen  14529  ccatvalfn  14535  swrdlen  14601  swrdwrdsymb  14616  swrdswrd  14659  sqrtf  15314  mptfzshft  15728  efcvgfsum  16033  prmreclem2  16854  1arith  16864  vdwlem6  16923  vdwlem8  16925  slotfn  17121  topnfn  17375  fnmre  17539  cidffn  17626  cidfn  17627  funcres  17850  initofn  17941  termofn  17942  zeroofn  17943  yonedainv  18238  fn0g  18588  smndex1igid  18821  smndex1n0mnd  18829  grpinvfn  18902  cycsubmel  19115  conjnmz  19166  psgnfn  19410  odf  19446  sylow1lem4  19510  pgpssslw  19523  sylow2blem3  19531  sylow3lem2  19537  cygctb  19801  dprd2da  19953  fnmgp  20030  rlmfn  20957  rrgsupp  21107  frlmup4  21575  asclfn  21654  evlslem1  21864  mdetrlin  22324  fncld  22746  hauseqlcld  23370  kqf  23471  filunirn  23606  fmf  23669  txflf  23730  clsnsg  23834  tgpconncomp  23837  qustgpopn  23844  qustgplem  23845  ustfn  23926  xmetunirn  24063  met1stc  24250  rrxmvallem  25145  ovolf  25223  vitali  25354  i1fmulc  25445  mbfi1fseqlem4  25460  itg2seq  25484  itg2monolem1  25492  i1fibl  25549  fncpn  25674  lhop1lem  25754  mdegxrf  25810  aannenlem3  26067  efabl  26283  logccv  26395  gausslemma2dlem1  27093  padicabvf  27358  mptelee  28408  wlkiswwlks2lem1  29378  clwlkclwwlklem2a2  29501  grpoinvf  30040  occllem  30811  pjfni  31209  pjmfn  31223  rnbra  31615  bra11  31616  kbass2  31625  hmopidmchi  31659  xppreima2  32131  abfmpunirn  32132  psgnfzto1stlem  32517  ghmquskerco  32791  elrspunidl  32808  locfinreflem  33106  zarclsint  33138  zar0ring  33144  rhmpreimacn  33151  ofcfn  33384  sxbrsigalem3  33557  eulerpartgbij  33657  sseqfv1  33674  sseqfn  33675  sseqf  33677  sseqfv2  33679  signstlen  33864  msubrn  34806  msrf  34819  faclimlem1  35005  bj-evalfn  36258  bj-inftyexpitaufo  36386  matunitlindflem1  36787  poimirlem30  36821  mblfinlem2  36829  volsupnfl  36836  cnambfre  36839  itg2addnclem2  36843  itg2addnclem3  36844  ftc1anclem5  36868  ftc1anclem7  36870  sdclem2  36913  prdsbnd2  36966  rrncmslem  37003  diafn  40208  cdlemm10N  40292  dibfna  40328  lcfrlem9  40724  mapd1o  40822  hdmapfnN  41003  hgmapfnN  41062  evlsvvval  41437  fsuppind  41464  rmxypairf1o  41952  hbtlem6  42173  dgraaf  42191  cytpfn  42252  tfsconcatrev  42400  ntrf  43176  uzmptshftfval  43407  binomcxplemrat  43411  addrfn  43533  subrfn  43534  mulvfn  43535  limsup10exlem  44787  liminfvalxr  44798  fourierdlem62  45183  fourierdlem70  45191  fourierdlem71  45192  fmtnorn  46501  zrinitorngc  46987  zrtermorngc  46988  zrtermoringc  47057