Theorem fnmpti 6679

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  ∀wral 3085  Vcvv 3463   ↦ cmpt 5196   Fn wfn 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-fun 6539  df-fn 6540

This theorem is referenced by:  dmmpti  6680  fconst  6765  dffn5  6940  idref  7143  eufnfv  7228  offn  7688  caofinvl  7707  fo1st  8006  fo2nd  8007  reldm  8041  fimaproj  8131  mapsnf1o2  8892  unfilem2  9266  fidomdm  9291  noinfep  9629  ssttrcl  9684  ttrcltr  9685  ttrclselem2  9695  aceq3lem  10104  dfac4  10106  ackbij2lem2  10222  cfslb2n  10252  axcc2lem  10420  dmct  10508  konigthlem  10553  rankcf  10762  tskuni  10768  seqf1o  14079  ccatlen  14612  ccatvalfn  14618  swrdlen  14685  swrdwrdsymb  14700  swrdswrd  14742  sqrtf  15415  mptfzshft  15829  efcvgfsum  16140  prmreclem2  16977  1arith  16987  vdwlem6  17046  vdwlem8  17048  slotfn  17244  topnfn  17478  fnmre  17643  cidffn  17734  cidfn  17735  funcres  17953  initofn  18044  termofn  18045  zeroofn  18046  yonedainv  18337  fn0g  18721  smndex1igid  18965  smndex1igidOLD  18966  smndex1n0mnd  18974  grpinvfn  19048  cycsubmel  19271  conjnmz  19322  ghmquskerco  19354  psgnfn  19571  odf  19607  sylow1lem4  19671  pgpssslw  19684  sylow2blem3  19692  sylow3lem2  19698  cygctb  19962  dprd2da  20114  fnmgp  20218  zrinitorngc  20727  zrtermorngc  20728  zrtermoringc  20760  rrgsupp  20786  rlmfn  21289  frlmup4  21920  asclfn  21999  evlslem1  22202  evlsvvval  22213  psdmplcl  22294  psdadd  22295  psdmul  22298  psdmvr  22301  mdetrlin  22728  fncld  23148  hauseqlcld  23772  kqf  23873  filunirn  24008  fmf  24071  txflf  24132  clsnsg  24236  tgpconncomp  24239  qustgpopn  24246  qustgplem  24247  ustfn  24328  xmetunirn  24463  met1stc  24647  rrxmvallem  25532  ovolf  25610  vitali  25741  i1fmulc  25831  mbfi1fseqlem4  25846  itg2seq  25870  itg2monolem1  25878  i1fibl  25936  fncpn  26061  lhop1lem  26141  mdegxrf  26194  aannenlem3  26460  efabl  26681  logccv  26794  gausslemma2dlem1  27496  padicabvf  27761  mpteleeOLD  29186  wlkiswwlks2lem1  30159  clwlkclwwlklem2a2  30285  grpoinvf  30825  occllem  31596  pjfni  31994  pjmfn  32008  rnbra  32400  bra11  32401  kbass2  32410  hmopidmchi  32444  xppreima2  32937  abfmpunirn  32938  psgnfzto1stlem  33361  elrspunidl  33680  locfinreflem  34175  zarclsint  34207  zar0ring  34213  rhmpreimacn  34220  ofcfn  34435  sxbrsigalem3  34607  eulerpartgbij  34707  sseqfv1  34724  sseqfn  34725  sseqf  34727  sseqfv2  34729  signstlen  34899  kardfn  35497  vonf1oonfo  35532  msubrn  35954  msrf  35967  faclimlem1  36168  weiunlem  36897  bj-evalfn  37637  bj-inftyexpitaufo  37768  matunitlindflem1  38189  poimirlem30  38223  mblfinlem2  38231  volsupnfl  38238  cnambfre  38241  itg2addnclem2  38245  itg2addnclem3  38246  ftc1anclem5  38270  ftc1anclem7  38272  sdclem2  38315  prdsbnd2  38368  rrncmslem  38405  diafn  41732  cdlemm10N  41816  dibfna  41852  lcfrlem9  42248  mapd1o  42346  hdmapfnN  42527  hgmapfnN  42586  fsuppind  43248  rmxypairf1o  43564  hbtlem6  43782  dgraaf  43800  cytpfn  43854  tfsconcatrev  44001  ntrf  44775  uzmptshftfval  44982  binomcxplemrat  44986  addrfn  45106  subrfn  45107  mulvfn  45108  limsup10exlem  46412  liminfvalxr  46423  fourierdlem62  46808  fourierdlem70  46816  fourierdlem71  46817  nthrucw  47528  cjnpoly  47549  fmtnorn  48209  tposideq  49585  cicfn  49739  fucofn22  50037  fucoid  50045  dfinito4  50198