Theorem fnmpti 6625

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3436   ↦ cmpt 5173   Fn wfn 6477

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-fun 6484  df-fn 6485

This theorem is referenced by:  dmmpti  6626  fconst  6710  dffn5  6881  idref  7080  eufnfv  7165  offn  7626  caofinvl  7645  fo1st  7944  fo2nd  7945  reldm  7979  fimaproj  8068  mapsnf1o2  8821  unfilem2  9195  fidomdm  9224  noinfep  9556  ssttrcl  9611  ttrcltr  9612  ttrclselem2  9622  aceq3lem  10014  dfac4  10016  ackbij2lem2  10133  cfslb2n  10162  axcc2lem  10330  dmct  10418  konigthlem  10462  rankcf  10671  tskuni  10677  seqf1o  13950  ccatlen  14482  ccatvalfn  14488  swrdlen  14554  swrdwrdsymb  14569  swrdswrd  14611  sqrtf  15271  mptfzshft  15685  efcvgfsum  15993  prmreclem2  16829  1arith  16839  vdwlem6  16898  vdwlem8  16900  slotfn  17095  topnfn  17329  fnmre  17493  cidffn  17584  cidfn  17585  funcres  17803  initofn  17894  termofn  17895  zeroofn  17896  yonedainv  18187  fn0g  18537  smndex1igid  18778  smndex1n0mnd  18786  grpinvfn  18860  cycsubmel  19079  conjnmz  19131  ghmquskerco  19163  psgnfn  19380  odf  19416  sylow1lem4  19480  pgpssslw  19493  sylow2blem3  19501  sylow3lem2  19507  cygctb  19771  dprd2da  19923  fnmgp  20027  zrinitorngc  20527  zrtermorngc  20528  zrtermoringc  20560  rrgsupp  20586  rlmfn  21094  frlmup4  21708  asclfn  21788  evlslem1  21987  psdmplcl  22047  psdadd  22048  psdmul  22051  psdmvr  22054  mdetrlin  22487  fncld  22907  hauseqlcld  23531  kqf  23632  filunirn  23767  fmf  23830  txflf  23891  clsnsg  23995  tgpconncomp  23998  qustgpopn  24005  qustgplem  24006  ustfn  24087  xmetunirn  24223  met1stc  24407  rrxmvallem  25302  ovolf  25381  vitali  25512  i1fmulc  25602  mbfi1fseqlem4  25617  itg2seq  25641  itg2monolem1  25649  i1fibl  25707  fncpn  25833  lhop1lem  25916  mdegxrf  25971  aannenlem3  26236  efabl  26457  logccv  26570  gausslemma2dlem1  27275  padicabvf  27540  mptelee  28840  wlkiswwlks2lem1  29814  clwlkclwwlklem2a2  29937  grpoinvf  30476  occllem  31247  pjfni  31645  pjmfn  31659  rnbra  32051  bra11  32052  kbass2  32061  hmopidmchi  32095  xppreima2  32595  abfmpunirn  32596  psgnfzto1stlem  33043  elrspunidl  33366  locfinreflem  33813  zarclsint  33845  zar0ring  33851  rhmpreimacn  33858  ofcfn  34073  sxbrsigalem3  34246  eulerpartgbij  34346  sseqfv1  34363  sseqfn  34364  sseqf  34366  sseqfv2  34368  signstlen  34541  msubrn  35512  msrf  35525  faclimlem1  35726  weiunlem2  36447  bj-evalfn  37058  bj-inftyexpitaufo  37186  matunitlindflem1  37606  poimirlem30  37640  mblfinlem2  37648  volsupnfl  37655  cnambfre  37658  itg2addnclem2  37662  itg2addnclem3  37663  ftc1anclem5  37687  ftc1anclem7  37689  sdclem2  37732  prdsbnd2  37785  rrncmslem  37822  diafn  41023  cdlemm10N  41107  dibfna  41143  lcfrlem9  41539  mapd1o  41637  hdmapfnN  41818  hgmapfnN  41877  evlsvvval  42546  fsuppind  42573  rmxypairf1o  42894  hbtlem6  43112  dgraaf  43130  cytpfn  43184  tfsconcatrev  43331  ntrf  44106  uzmptshftfval  44329  binomcxplemrat  44333  addrfn  44455  subrfn  44456  mulvfn  44457  limsup10exlem  45763  liminfvalxr  45774  fourierdlem62  46159  fourierdlem70  46167  fourierdlem71  46168  cjnpoly  46883  fmtnorn  47528  tposideq  48882  cicfn  49037  fucofn22  49335  fucoid  49343  dfinito4  49496