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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3444   ↦ cmpt 5183   Fn wfn 6494

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6501  df-fn 6502

This theorem is referenced by:  dmmpti  6644  fconst  6728  dffn5  6901  idref  7100  eufnfv  7185  offn  7646  caofinvl  7665  fo1st  7967  fo2nd  7968  reldm  8002  fimaproj  8091  mapsnf1o2  8844  unfilem2  9231  fidomdm  9261  noinfep  9589  ssttrcl  9644  ttrcltr  9645  ttrclselem2  9655  aceq3lem  10049  dfac4  10051  ackbij2lem2  10168  cfslb2n  10197  axcc2lem  10365  dmct  10453  konigthlem  10497  rankcf  10706  tskuni  10712  seqf1o  13984  ccatlen  14516  ccatvalfn  14522  swrdlen  14588  swrdwrdsymb  14603  swrdswrd  14646  sqrtf  15306  mptfzshft  15720  efcvgfsum  16028  prmreclem2  16864  1arith  16874  vdwlem6  16933  vdwlem8  16935  slotfn  17130  topnfn  17364  fnmre  17528  cidffn  17619  cidfn  17620  funcres  17838  initofn  17929  termofn  17930  zeroofn  17931  yonedainv  18222  fn0g  18572  smndex1igid  18813  smndex1n0mnd  18821  grpinvfn  18895  cycsubmel  19114  conjnmz  19166  ghmquskerco  19198  psgnfn  19415  odf  19451  sylow1lem4  19515  pgpssslw  19528  sylow2blem3  19536  sylow3lem2  19542  cygctb  19806  dprd2da  19958  fnmgp  20062  zrinitorngc  20562  zrtermorngc  20563  zrtermoringc  20595  rrgsupp  20621  rlmfn  21129  frlmup4  21743  asclfn  21823  evlslem1  22022  psdmplcl  22082  psdadd  22083  psdmul  22086  psdmvr  22089  mdetrlin  22522  fncld  22942  hauseqlcld  23566  kqf  23667  filunirn  23802  fmf  23865  txflf  23926  clsnsg  24030  tgpconncomp  24033  qustgpopn  24040  qustgplem  24041  ustfn  24122  xmetunirn  24258  met1stc  24442  rrxmvallem  25337  ovolf  25416  vitali  25547  i1fmulc  25637  mbfi1fseqlem4  25652  itg2seq  25676  itg2monolem1  25684  i1fibl  25742  fncpn  25868  lhop1lem  25951  mdegxrf  26006  aannenlem3  26271  efabl  26492  logccv  26605  gausslemma2dlem1  27310  padicabvf  27575  mptelee  28875  wlkiswwlks2lem1  29849  clwlkclwwlklem2a2  29972  grpoinvf  30511  occllem  31282  pjfni  31680  pjmfn  31694  rnbra  32086  bra11  32087  kbass2  32096  hmopidmchi  32130  xppreima2  32625  abfmpunirn  32626  psgnfzto1stlem  33072  elrspunidl  33392  locfinreflem  33823  zarclsint  33855  zar0ring  33861  rhmpreimacn  33868  ofcfn  34083  sxbrsigalem3  34256  eulerpartgbij  34356  sseqfv1  34373  sseqfn  34374  sseqf  34376  sseqfv2  34378  signstlen  34551  msubrn  35509  msrf  35522  faclimlem1  35723  weiunlem2  36444  bj-evalfn  37055  bj-inftyexpitaufo  37183  matunitlindflem1  37603  poimirlem30  37637  mblfinlem2  37645  volsupnfl  37652  cnambfre  37655  itg2addnclem2  37659  itg2addnclem3  37660  ftc1anclem5  37684  ftc1anclem7  37686  sdclem2  37729  prdsbnd2  37782  rrncmslem  37819  diafn  41021  cdlemm10N  41105  dibfna  41141  lcfrlem9  41537  mapd1o  41635  hdmapfnN  41816  hgmapfnN  41875  evlsvvval  42544  fsuppind  42571  rmxypairf1o  42893  hbtlem6  43111  dgraaf  43129  cytpfn  43183  tfsconcatrev  43330  ntrf  44105  uzmptshftfval  44328  binomcxplemrat  44332  addrfn  44454  subrfn  44455  mulvfn  44456  limsup10exlem  45763  liminfvalxr  45774  fourierdlem62  46159  fourierdlem70  46167  fourierdlem71  46168  cjnpoly  46883  fmtnorn  47528  tposideq  48869  cicfn  49024  fucofn22  49322  fucoid  49330  dfinito4  49483