Theorem fnmpti 6661

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447   ↦ cmpt 5188   Fn wfn 6506

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  dmmpti  6662  fconst  6746  dffn5  6919  idref  7118  eufnfv  7203  offn  7666  caofinvl  7685  fo1st  7988  fo2nd  7989  reldm  8023  fimaproj  8114  mapsnf1o2  8867  unfilem2  9255  fidomdm  9285  noinfep  9613  ssttrcl  9668  ttrcltr  9669  ttrclselem2  9679  aceq3lem  10073  dfac4  10075  ackbij2lem2  10192  cfslb2n  10221  axcc2lem  10389  dmct  10477  konigthlem  10521  rankcf  10730  tskuni  10736  seqf1o  14008  ccatlen  14540  ccatvalfn  14546  swrdlen  14612  swrdwrdsymb  14627  swrdswrd  14670  sqrtf  15330  mptfzshft  15744  efcvgfsum  16052  prmreclem2  16888  1arith  16898  vdwlem6  16957  vdwlem8  16959  slotfn  17154  topnfn  17388  fnmre  17552  cidffn  17639  cidfn  17640  funcres  17858  initofn  17949  termofn  17950  zeroofn  17951  yonedainv  18242  fn0g  18590  smndex1igid  18831  smndex1n0mnd  18839  grpinvfn  18913  cycsubmel  19132  conjnmz  19184  ghmquskerco  19216  psgnfn  19431  odf  19467  sylow1lem4  19531  pgpssslw  19544  sylow2blem3  19552  sylow3lem2  19558  cygctb  19822  dprd2da  19974  fnmgp  20051  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  rrgsupp  20610  rlmfn  21097  frlmup4  21710  asclfn  21790  evlslem1  21989  psdmplcl  22049  psdadd  22050  psdmul  22053  psdmvr  22056  mdetrlin  22489  fncld  22909  hauseqlcld  23533  kqf  23634  filunirn  23769  fmf  23832  txflf  23893  clsnsg  23997  tgpconncomp  24000  qustgpopn  24007  qustgplem  24008  ustfn  24089  xmetunirn  24225  met1stc  24409  rrxmvallem  25304  ovolf  25383  vitali  25514  i1fmulc  25604  mbfi1fseqlem4  25619  itg2seq  25643  itg2monolem1  25651  i1fibl  25709  fncpn  25835  lhop1lem  25918  mdegxrf  25973  aannenlem3  26238  efabl  26459  logccv  26572  gausslemma2dlem1  27277  padicabvf  27542  mptelee  28822  wlkiswwlks2lem1  29799  clwlkclwwlklem2a2  29922  grpoinvf  30461  occllem  31232  pjfni  31630  pjmfn  31644  rnbra  32036  bra11  32037  kbass2  32046  hmopidmchi  32080  xppreima2  32575  abfmpunirn  32576  psgnfzto1stlem  33057  elrspunidl  33399  locfinreflem  33830  zarclsint  33862  zar0ring  33868  rhmpreimacn  33875  ofcfn  34090  sxbrsigalem3  34263  eulerpartgbij  34363  sseqfv1  34380  sseqfn  34381  sseqf  34383  sseqfv2  34385  signstlen  34558  msubrn  35516  msrf  35529  faclimlem1  35730  weiunlem2  36451  bj-evalfn  37062  bj-inftyexpitaufo  37190  matunitlindflem1  37610  poimirlem30  37644  mblfinlem2  37652  volsupnfl  37659  cnambfre  37662  itg2addnclem2  37666  itg2addnclem3  37667  ftc1anclem5  37691  ftc1anclem7  37693  sdclem2  37736  prdsbnd2  37789  rrncmslem  37826  diafn  41028  cdlemm10N  41112  dibfna  41148  lcfrlem9  41544  mapd1o  41642  hdmapfnN  41823  hgmapfnN  41882  evlsvvval  42551  fsuppind  42578  rmxypairf1o  42900  hbtlem6  43118  dgraaf  43136  cytpfn  43190  tfsconcatrev  43337  ntrf  44112  uzmptshftfval  44335  binomcxplemrat  44339  addrfn  44461  subrfn  44462  mulvfn  44463  limsup10exlem  45770  liminfvalxr  45781  fourierdlem62  46166  fourierdlem70  46174  fourierdlem71  46175  cjnpoly  46890  fmtnorn  47535  tposideq  48876  cicfn  49031  fucofn22  49329  fucoid  49337  dfinito4  49490