Theorem fnmpti 6665

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

Syntax hints:   = wceq 1561   ∈ wcel 2143  ∀wral 3077  Vcvv 3455   ↦ cmpt 5182   Fn wfn 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-fun 6524  df-fn 6525

This theorem is referenced by:  dmmpti  6666  fconst  6751  dffn5  6926  idref  7129  eufnfv  7214  offn  7674  caofinvl  7693  fo1st  7991  fo2nd  7992  reldm  8026  fimaproj  8116  mapsnf1o2  8877  unfilem2  9251  fidomdm  9278  noinfep  9616  ssttrcl  9671  ttrcltr  9672  ttrclselem2  9682  aceq3lem  10077  dfac4  10079  ackbij2lem2  10196  cfslb2n  10226  axcc2lem  10394  dmct  10482  konigthlem  10527  rankcf  10736  tskuni  10742  seqf1o  14057  ccatlen  14589  ccatvalfn  14595  swrdlen  14662  swrdwrdsymb  14677  swrdswrd  14719  sqrtf  15392  mptfzshft  15806  efcvgfsum  16117  prmreclem2  16954  1arith  16964  vdwlem6  17023  vdwlem8  17025  slotfn  17221  topnfn  17455  fnmre  17620  cidffn  17711  cidfn  17712  funcres  17930  initofn  18021  termofn  18022  zeroofn  18023  yonedainv  18314  fn0g  18698  smndex1igid  18941  smndex1igidOLD  18942  smndex1n0mnd  18950  grpinvfn  19024  cycsubmel  19242  conjnmz  19293  ghmquskerco  19325  psgnfn  19542  odf  19578  sylow1lem4  19642  pgpssslw  19655  sylow2blem3  19663  sylow3lem2  19669  cygctb  19933  dprd2da  20085  fnmgp  20189  zrinitorngc  20693  zrtermorngc  20694  zrtermoringc  20726  rrgsupp  20752  rlmfn  21258  frlmup4  21854  asclfn  21933  evlslem1  22136  evlsvvval  22147  psdmplcl  22228  psdadd  22229  psdmul  22232  psdmvr  22235  mdetrlin  22663  fncld  23083  hauseqlcld  23707  kqf  23808  filunirn  23943  fmf  24006  txflf  24067  clsnsg  24171  tgpconncomp  24174  qustgpopn  24181  qustgplem  24182  ustfn  24263  xmetunirn  24398  met1stc  24582  rrxmvallem  25467  ovolf  25545  vitali  25676  i1fmulc  25766  mbfi1fseqlem4  25781  itg2seq  25805  itg2monolem1  25813  i1fibl  25871  fncpn  25996  lhop1lem  26076  mdegxrf  26129  aannenlem3  26395  efabl  26616  logccv  26729  gausslemma2dlem1  27431  padicabvf  27696  mpteleeOLD  29097  wlkiswwlks2lem1  30070  clwlkclwwlklem2a2  30196  grpoinvf  30736  occllem  31507  pjfni  31905  pjmfn  31919  rnbra  32311  bra11  32312  kbass2  32321  hmopidmchi  32355  xppreima2  32854  abfmpunirn  32855  psgnfzto1stlem  33281  elrspunidl  33615  locfinreflem  34138  zarclsint  34170  zar0ring  34176  rhmpreimacn  34183  ofcfn  34398  sxbrsigalem3  34570  eulerpartgbij  34670  sseqfv1  34687  sseqfn  34688  sseqf  34690  sseqfv2  34692  signstlen  34862  vonf1oonfo  35459  msubrn  35880  msrf  35893  faclimlem1  36094  weiunlem  36824  bj-evalfn  37564  bj-inftyexpitaufo  37695  matunitlindflem1  38116  poimirlem30  38150  mblfinlem2  38158  volsupnfl  38165  cnambfre  38168  itg2addnclem2  38172  itg2addnclem3  38173  ftc1anclem5  38197  ftc1anclem7  38199  sdclem2  38242  prdsbnd2  38295  rrncmslem  38332  diafn  41659  cdlemm10N  41743  dibfna  41779  lcfrlem9  42175  mapd1o  42273  hdmapfnN  42454  hgmapfnN  42513  fsuppind  43173  rmxypairf1o  43489  hbtlem6  43707  dgraaf  43725  cytpfn  43779  tfsconcatrev  43926  ntrf  44700  uzmptshftfval  44923  binomcxplemrat  44927  addrfn  45048  subrfn  45049  mulvfn  45050  limsup10exlem  46347  liminfvalxr  46358  fourierdlem62  46743  fourierdlem70  46751  fourierdlem71  46752  nthrucw  47463  cjnpoly  47484  fmtnorn  48144  tposideq  49510  cicfn  49664  fucofn22  49962  fucoid  49970  dfinito4  50123