Theorem fnmpti 6060

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

Syntax hints:   = wceq 1523   ∈ wcel 2030  ∀wral 2941  Vcvv 3231   ↦ cmpt 4762   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-fun 5928  df-fn 5929

This theorem is referenced by:  dmmpti  6061  fconst  6129  dffn5  6280  eufnfv  6531  idref  6539  offn  6950  caofinvl  6966  fo1st  7230  fo2nd  7231  reldm  7263  mapsnf1o2  7947  unfilem2  8266  fidomdm  8284  pwfilem  8301  noinfep  8595  aceq3lem  8981  dfac4  8983  ackbij2lem2  9100  cfslb2n  9128  axcc2lem  9296  dmct  9384  konigthlem  9428  rankcf  9637  tskuni  9643  seqf1o  12882  ccatlen  13393  ccatvalfn  13399  swrdlen  13468  swrdswrd  13506  sqrtf  14147  mptfzshft  14554  fsumrev  14555  fprodrev  14751  efcvgfsum  14860  prmreclem2  15668  1arith  15678  vdwlem6  15737  vdwlem8  15739  slotfn  15922  topnfn  16133  fnmre  16298  cidffn  16386  cidfn  16387  funcres  16603  yonedainv  16968  fn0g  17309  grpinvfn  17509  conjnmz  17741  psgnfn  17967  odf  18002  sylow1lem4  18062  pgpssslw  18075  sylow2blem3  18083  sylow3lem2  18089  cygctb  18339  dprd2da  18487  fnmgp  18537  rlmfn  19238  rrgsupp  19339  asclfn  19384  evlslem1  19563  frlmup4  20188  mdetrlin  20456  fncld  20874  hauseqlcld  21497  kqf  21598  filunirn  21733  fmf  21796  txflf  21857  clsnsg  21960  tgpconncomp  21963  qustgpopn  21970  qustgplem  21971  ustfn  22052  xmetunirn  22189  met1stc  22373  rrxmvallem  23233  ovolf  23296  vitali  23427  i1fmulc  23515  mbfi1fseqlem4  23530  itg2seq  23554  itg2monolem1  23562  i1fibl  23619  fncpn  23741  lhop1lem  23821  mdegxrf  23873  aannenlem3  24130  efabl  24341  logccv  24454  gausslemma2dlem1  25136  padicabvf  25365  mptelee  25820  wlkiswwlks2lem1  26823  clwlkclwwlklem2a2  26959  grpoinvf  27514  occllem  28290  pjfni  28688  pjmfn  28702  rnbra  29094  bra11  29095  kbass2  29104  hmopidmchi  29138  xppreima2  29578  abfmpunirn  29580  psgnfzto1stlem  29978  fimaproj  30028  locfinreflem  30035  ofcfn  30290  sxbrsigalem3  30462  eulerpartgbij  30562  sseqfv1  30579  sseqfn  30580  sseqf  30582  sseqfv2  30584  signstlen  30772  msubrn  31552  msrf  31565  faclimlem1  31755  bj-evalfn  33151  matunitlindflem1  33535  poimirlem30  33569  mblfinlem2  33577  volsupnfl  33584  cnambfre  33588  itg2addnclem2  33592  itg2addnclem3  33593  ftc1anclem5  33619  ftc1anclem7  33621  sdclem2  33668  prdsbnd2  33724  rrncmslem  33761  diafn  36640  cdlemm10N  36724  dibfna  36760  lcfrlem9  37156  mapd1o  37254  hdmapfnN  37438  hgmapfnN  37497  rmxypairf1o  37793  hbtlem6  38016  dgraaf  38034  cytpfn  38103  ntrf  38738  uzmptshftfval  38862  binomcxplemrat  38866  addrfn  38993  subrfn  38994  mulvfn  38995  limsup10exlem  40322  liminfvalxr  40333  fourierdlem62  40703  fourierdlem70  40711  fourierdlem71  40712  fmtnorn  41771  zrinitorngc  42325  zrtermorngc  42326  zrtermoringc  42395