Theorem fnmpti 6676

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ↦ cmpt 5186   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6535  df-fn 6536

This theorem is used by:  dmmpti  6677  fconst  6762  dffn5  6937  idref  7143  eufnfv  7229  offn  7692  caofinvl  7711  fo1st  8007  fo2nd  8008  reldm  8042  fimaproj  8134  mapsnf1o2  8904  unfilem2  9279  fidomdm  9304  noinfep  9642  ssttrcl  9697  ttrcltr  9698  ttrclselem2  9708  aceq3lem  10126  dfac4  10128  ackbij2lem2  10244  cfslb2n  10273  axcc2lem  10441  dmct  10529  dmctOLD  10530  konigthlem  10580  rankcf  10789  tskuni  10795  seqf1o  14110  ccatlen  14643  ccatvalfn  14649  swrdlen  14718  swrdwrdsymb  14735  swrdswrd  14777  sqrtf  15454  mptfzshft  15867  efcvgfsum  16175  prmreclem2  17012  1arith  17022  vdwlem6  17081  vdwlem8  17083  slotfn  17279  topnfn  17513  fnmre  17678  cidffn  17769  cidfn  17770  funcres  17988  initofn  18079  termofn  18080  zeroofn  18081  yonedainv  18372  fn0g  18759  smndex1igid  19018  smndex1igidOLD  19019  smndex1n0mnd  19027  grpinvfn  19108  cycsubmel  19331  conjnmz  19382  ghmquskerco  19414  psgnfn  19631  odf  19667  sylow1lem4  19731  pgpssslw  19744  sylow2blem3  19752  sylow3lem2  19758  cygctb  20022  dprd2da  20174  fnmgp  20278  zrinitorngc  20807  zrtermorngc  20808  zrtermoringc  20840  rrgsupp  20866  rlmfn  21377  frlmup4  22017  asclfn  22098  evlslem1  22301  evlsvvval  22312  psdmplcl  22393  psdadd  22394  psdmul  22397  psdmvr  22400  mdetrlin  22827  matunitlindflem1  22904  fncld  23250  hauseqlcld  23875  kqf  23976  filunirn  24111  fmf  24174  txflf  24235  clsnsg  24339  tgpconncomp  24342  qustgpopn  24349  qustgplem  24350  ustfn  24431  xmetunirn  24566  met1stc  24750  rrxmvallem  25635  ovolf  25713  vitali  25844  i1fmulc  25934  mbfi1fseqlem4  25949  itg2seq  25973  itg2monolem1  25981  i1fibl  26038  fncpn  26163  lhop1lem  26243  mdegxrf  26296  aannenlem3  26569  efabl  26790  logccv  26903  gausslemma2dlem1  27605  padicabvf  27870  mpteleeOLD  29355  wlkiswwlks2lem1  30340  clwlkclwwlklem2a2  30466  grpoinvf  31016  occllem  31787  pjfni  32185  pjmfn  32199  rnbra  32591  bra11  32592  kbass2  32601  hmopidmchi  32635  xppreima2  33127  abfmpunirn  33128  psgnfzto1stlem  33543  elrspunidl  33859  locfinreflem  34353  zarclsint  34385  zar0ring  34391  rhmpreimacn  34398  ofcfn  34613  sxbrsigalem3  34786  eulerpartgbij  34886  sseqfv1  34903  sseqfn  34904  sseqf  34906  sseqfv2  34908  signstlen  35078  kardfn  35680  vonf1oonfo  35715  msubrn  36111  msrf  36124  faclimlem1  36325  weiunlem  37085  bj-evalfn  37826  bj-inftyexpitaufo  37957  poimirlem30  38402  mblfinlem2  38410  volsupnfl  38417  cnambfre  38420  itg2addnclem2  38424  itg2addnclem3  38425  ftc1anclem5  38449  ftc1anclem7  38451  sdclem2  38495  prdsbnd2  38548  rrncmslem  38585  diafn  41910  cdlemm10N  41994  dibfna  42030  lcfrlem9  42426  mapd1o  42524  hdmapfnN  42705  hgmapfnN  42764  fsuppind  43439  rmxypairf1o  43755  hbtlem6  43973  dgraaf  43991  cytpfn  44045  tfsconcatrev  44192  ntrf  44966  uzmptshftfval  45173  binomcxplemrat  45177  addrfn  45297  subrfn  45298  mulvfn  45299  limsup10exlem  46603  liminfvalxr  46614  fourierdlem62  46999  fourierdlem70  47007  fourierdlem71  47008  cjnpoly  47760  fmtnorn  48440  tposideq  49817  cicfn  49971  fucofn22  50269  fucoid  50277  dfinito4  50430  crosspaltd  50802  crossp3d  50803  veronesevrowd  50815  veronesematrowd  50817  veroquadmodzerod  50820