Theorem fnmpti 6636

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430   ↦ cmpt 5167   Fn wfn 6488

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 5232  ax-pr 5371

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-fun 6495  df-fn 6496

This theorem is referenced by:  dmmpti  6637  fconst  6721  dffn5  6893  idref  7094  eufnfv  7178  offn  7638  caofinvl  7657  fo1st  7956  fo2nd  7957  reldm  7991  fimaproj  8079  mapsnf1o2  8836  unfilem2  9210  fidomdm  9238  noinfep  9575  ssttrcl  9630  ttrcltr  9631  ttrclselem2  9641  aceq3lem  10036  dfac4  10038  ackbij2lem2  10155  cfslb2n  10184  axcc2lem  10352  dmct  10440  konigthlem  10485  rankcf  10694  tskuni  10700  seqf1o  13999  ccatlen  14531  ccatvalfn  14537  swrdlen  14604  swrdwrdsymb  14619  swrdswrd  14661  sqrtf  15320  mptfzshft  15734  efcvgfsum  16045  prmreclem2  16882  1arith  16892  vdwlem6  16951  vdwlem8  16953  slotfn  17148  topnfn  17382  fnmre  17547  cidffn  17638  cidfn  17639  funcres  17857  initofn  17948  termofn  17949  zeroofn  17950  yonedainv  18241  fn0g  18625  smndex1igid  18868  smndex1igidOLD  18869  smndex1n0mnd  18877  grpinvfn  18951  cycsubmel  19169  conjnmz  19221  ghmquskerco  19253  psgnfn  19470  odf  19506  sylow1lem4  19570  pgpssslw  19583  sylow2blem3  19591  sylow3lem2  19597  cygctb  19861  dprd2da  20013  fnmgp  20117  zrinitorngc  20613  zrtermorngc  20614  zrtermoringc  20646  rrgsupp  20672  rlmfn  21180  frlmup4  21794  asclfn  21873  evlslem1  22073  evlsvvval  22084  psdmplcl  22141  psdadd  22142  psdmul  22145  psdmvr  22148  mdetrlin  22580  fncld  23000  hauseqlcld  23624  kqf  23725  filunirn  23860  fmf  23923  txflf  23984  clsnsg  24088  tgpconncomp  24091  qustgpopn  24098  qustgplem  24099  ustfn  24180  xmetunirn  24315  met1stc  24499  rrxmvallem  25384  ovolf  25462  vitali  25593  i1fmulc  25683  mbfi1fseqlem4  25698  itg2seq  25722  itg2monolem1  25730  i1fibl  25788  fncpn  25913  lhop1lem  25993  mdegxrf  26046  aannenlem3  26310  efabl  26530  logccv  26643  gausslemma2dlem1  27346  padicabvf  27611  mpteleeOLD  28981  wlkiswwlks2lem1  29955  clwlkclwwlklem2a2  30081  grpoinvf  30621  occllem  31392  pjfni  31790  pjmfn  31804  rnbra  32196  bra11  32197  kbass2  32206  hmopidmchi  32240  xppreima2  32742  abfmpunirn  32743  psgnfzto1stlem  33179  elrspunidl  33506  locfinreflem  34003  zarclsint  34035  zar0ring  34041  rhmpreimacn  34048  ofcfn  34263  sxbrsigalem3  34435  eulerpartgbij  34535  sseqfv1  34552  sseqfn  34553  sseqf  34555  sseqfv2  34557  signstlen  34730  msubrn  35730  msrf  35743  faclimlem1  35944  weiunlem  36664  bj-evalfn  37404  bj-inftyexpitaufo  37535  matunitlindflem1  37954  poimirlem30  37988  mblfinlem2  37996  volsupnfl  38003  cnambfre  38006  itg2addnclem2  38010  itg2addnclem3  38011  ftc1anclem5  38035  ftc1anclem7  38037  sdclem2  38080  prdsbnd2  38133  rrncmslem  38170  diafn  41497  cdlemm10N  41581  dibfna  41617  lcfrlem9  42013  mapd1o  42111  hdmapfnN  42292  hgmapfnN  42351  fsuppind  43040  rmxypairf1o  43360  hbtlem6  43578  dgraaf  43596  cytpfn  43650  tfsconcatrev  43797  ntrf  44571  uzmptshftfval  44794  binomcxplemrat  44798  addrfn  44919  subrfn  44920  mulvfn  44921  limsup10exlem  46221  liminfvalxr  46232  fourierdlem62  46617  fourierdlem70  46625  fourierdlem71  46626  nthrucw  47335  cjnpoly  47352  fmtnorn  48012  tposideq  49378  cicfn  49532  fucofn22  49830  fucoid  49838  dfinito4  49991