Theorem fnmpti 6635

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ↦ cmpt 5179   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  dmmpti  6636  fconst  6720  dffn5  6892  idref  7091  eufnfv  7175  offn  7635  caofinvl  7654  fo1st  7953  fo2nd  7954  reldm  7988  fimaproj  8077  mapsnf1o2  8832  unfilem2  9206  fidomdm  9234  noinfep  9569  ssttrcl  9624  ttrcltr  9625  ttrclselem2  9635  aceq3lem  10030  dfac4  10032  ackbij2lem2  10149  cfslb2n  10178  axcc2lem  10346  dmct  10434  konigthlem  10479  rankcf  10688  tskuni  10694  seqf1o  13966  ccatlen  14498  ccatvalfn  14504  swrdlen  14571  swrdwrdsymb  14586  swrdswrd  14628  sqrtf  15287  mptfzshft  15701  efcvgfsum  16009  prmreclem2  16845  1arith  16855  vdwlem6  16914  vdwlem8  16916  slotfn  17111  topnfn  17345  fnmre  17510  cidffn  17601  cidfn  17602  funcres  17820  initofn  17911  termofn  17912  zeroofn  17913  yonedainv  18204  fn0g  18588  smndex1igid  18829  smndex1n0mnd  18837  grpinvfn  18911  cycsubmel  19129  conjnmz  19181  ghmquskerco  19213  psgnfn  19430  odf  19466  sylow1lem4  19530  pgpssslw  19543  sylow2blem3  19551  sylow3lem2  19557  cygctb  19821  dprd2da  19973  fnmgp  20077  zrinitorngc  20575  zrtermorngc  20576  zrtermoringc  20608  rrgsupp  20634  rlmfn  21142  frlmup4  21756  asclfn  21836  evlslem1  22037  evlsvvval  22048  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  mdetrlin  22546  fncld  22966  hauseqlcld  23590  kqf  23691  filunirn  23826  fmf  23889  txflf  23950  clsnsg  24054  tgpconncomp  24057  qustgpopn  24064  qustgplem  24065  ustfn  24146  xmetunirn  24281  met1stc  24465  rrxmvallem  25360  ovolf  25439  vitali  25570  i1fmulc  25660  mbfi1fseqlem4  25675  itg2seq  25699  itg2monolem1  25707  i1fibl  25765  fncpn  25891  lhop1lem  25974  mdegxrf  26029  aannenlem3  26294  efabl  26515  logccv  26628  gausslemma2dlem1  27333  padicabvf  27598  mpteleeOLD  28968  wlkiswwlks2lem1  29942  clwlkclwwlklem2a2  30068  grpoinvf  30607  occllem  31378  pjfni  31776  pjmfn  31790  rnbra  32182  bra11  32183  kbass2  32192  hmopidmchi  32226  xppreima2  32729  abfmpunirn  32730  psgnfzto1stlem  33182  elrspunidl  33509  locfinreflem  33997  zarclsint  34029  zar0ring  34035  rhmpreimacn  34042  ofcfn  34257  sxbrsigalem3  34429  eulerpartgbij  34529  sseqfv1  34546  sseqfn  34547  sseqf  34549  sseqfv2  34551  signstlen  34724  msubrn  35723  msrf  35736  faclimlem1  35937  weiunlem  36657  bj-evalfn  37275  bj-inftyexpitaufo  37403  matunitlindflem1  37813  poimirlem30  37847  mblfinlem2  37855  volsupnfl  37862  cnambfre  37865  itg2addnclem2  37869  itg2addnclem3  37870  ftc1anclem5  37894  ftc1anclem7  37896  sdclem2  37939  prdsbnd2  37992  rrncmslem  38029  diafn  41290  cdlemm10N  41374  dibfna  41410  lcfrlem9  41806  mapd1o  41904  hdmapfnN  42085  hgmapfnN  42144  fsuppind  42829  rmxypairf1o  43149  hbtlem6  43367  dgraaf  43385  cytpfn  43439  tfsconcatrev  43586  ntrf  44360  uzmptshftfval  44583  binomcxplemrat  44587  addrfn  44708  subrfn  44709  mulvfn  44710  limsup10exlem  46012  liminfvalxr  46023  fourierdlem62  46408  fourierdlem70  46416  fourierdlem71  46417  nthrucw  47126  cjnpoly  47131  fmtnorn  47776  tposideq  49129  cicfn  49283  fucofn22  49581  fucoid  49589  dfinito4  49742