Theorem fnmpti 6643

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442   ↦ cmpt 5181   Fn wfn 6495

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  dmmpti  6644  fconst  6728  dffn5  6900  idref  7101  eufnfv  7185  offn  7645  caofinvl  7664  fo1st  7963  fo2nd  7964  reldm  7998  fimaproj  8087  mapsnf1o2  8844  unfilem2  9218  fidomdm  9246  noinfep  9581  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  aceq3lem  10042  dfac4  10044  ackbij2lem2  10161  cfslb2n  10190  axcc2lem  10358  dmct  10446  konigthlem  10491  rankcf  10700  tskuni  10706  seqf1o  13978  ccatlen  14510  ccatvalfn  14516  swrdlen  14583  swrdwrdsymb  14598  swrdswrd  14640  sqrtf  15299  mptfzshft  15713  efcvgfsum  16021  prmreclem2  16857  1arith  16867  vdwlem6  16926  vdwlem8  16928  slotfn  17123  topnfn  17357  fnmre  17522  cidffn  17613  cidfn  17614  funcres  17832  initofn  17923  termofn  17924  zeroofn  17925  yonedainv  18216  fn0g  18600  smndex1igid  18843  smndex1igidOLD  18844  smndex1n0mnd  18852  grpinvfn  18926  cycsubmel  19144  conjnmz  19196  ghmquskerco  19228  psgnfn  19445  odf  19481  sylow1lem4  19545  pgpssslw  19558  sylow2blem3  19566  sylow3lem2  19572  cygctb  19836  dprd2da  19988  fnmgp  20092  zrinitorngc  20590  zrtermorngc  20591  zrtermoringc  20623  rrgsupp  20649  rlmfn  21157  frlmup4  21771  asclfn  21851  evlslem1  22052  evlsvvval  22063  psdmplcl  22120  psdadd  22121  psdmul  22124  psdmvr  22127  mdetrlin  22561  fncld  22981  hauseqlcld  23605  kqf  23706  filunirn  23841  fmf  23904  txflf  23965  clsnsg  24069  tgpconncomp  24072  qustgpopn  24079  qustgplem  24080  ustfn  24161  xmetunirn  24296  met1stc  24480  rrxmvallem  25375  ovolf  25454  vitali  25585  i1fmulc  25675  mbfi1fseqlem4  25690  itg2seq  25714  itg2monolem1  25722  i1fibl  25780  fncpn  25906  lhop1lem  25989  mdegxrf  26044  aannenlem3  26309  efabl  26530  logccv  26643  gausslemma2dlem1  27348  padicabvf  27613  mpteleeOLD  28984  wlkiswwlks2lem1  29958  clwlkclwwlklem2a2  30084  grpoinvf  30624  occllem  31395  pjfni  31793  pjmfn  31807  rnbra  32199  bra11  32200  kbass2  32209  hmopidmchi  32243  xppreima2  32745  abfmpunirn  32746  psgnfzto1stlem  33198  elrspunidl  33525  locfinreflem  34022  zarclsint  34054  zar0ring  34060  rhmpreimacn  34067  ofcfn  34282  sxbrsigalem3  34454  eulerpartgbij  34554  sseqfv1  34571  sseqfn  34572  sseqf  34574  sseqfv2  34576  signstlen  34749  msubrn  35749  msrf  35762  faclimlem1  35963  weiunlem  36683  bj-evalfn  37330  bj-inftyexpitaufo  37461  matunitlindflem1  37871  poimirlem30  37905  mblfinlem2  37913  volsupnfl  37920  cnambfre  37923  itg2addnclem2  37927  itg2addnclem3  37928  ftc1anclem5  37952  ftc1anclem7  37954  sdclem2  37997  prdsbnd2  38050  rrncmslem  38087  diafn  41414  cdlemm10N  41498  dibfna  41534  lcfrlem9  41930  mapd1o  42028  hdmapfnN  42209  hgmapfnN  42268  fsuppind  42952  rmxypairf1o  43272  hbtlem6  43490  dgraaf  43508  cytpfn  43562  tfsconcatrev  43709  ntrf  44483  uzmptshftfval  44706  binomcxplemrat  44710  addrfn  44831  subrfn  44832  mulvfn  44833  limsup10exlem  46134  liminfvalxr  46145  fourierdlem62  46530  fourierdlem70  46538  fourierdlem71  46539  nthrucw  47248  cjnpoly  47253  fmtnorn  47898  tposideq  49251  cicfn  49405  fucofn22  49703  fucoid  49711  dfinito4  49864