Theorem fnmpti 6682

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  ∀wral 3082  Vcvv 3458   ↦ cmpt 5195   Fn wfn 6535

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-pr 5407

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-fun 6542  df-fn 6543

This theorem is used by:  dmmpti  6683  fconst  6768  dffn5  6943  idref  7146  eufnfv  7231  offn  7693  caofinvl  7712  fo1st  8008  fo2nd  8009  reldm  8043  fimaproj  8133  mapsnf1o2  8894  unfilem2  9268  fidomdm  9293  noinfep  9631  ssttrcl  9686  ttrcltr  9687  ttrclselem2  9697  aceq3lem  10115  dfac4  10117  ackbij2lem2  10233  cfslb2n  10262  axcc2lem  10430  dmct  10518  konigthlem  10563  rankcf  10772  tskuni  10778  seqf1o  14090  ccatlen  14623  ccatvalfn  14629  swrdlen  14696  swrdwrdsymb  14711  swrdswrd  14753  sqrtf  15426  mptfzshft  15840  efcvgfsum  16150  prmreclem2  16987  1arith  16997  vdwlem6  17056  vdwlem8  17058  slotfn  17254  topnfn  17488  fnmre  17653  cidffn  17744  cidfn  17745  funcres  17963  initofn  18054  termofn  18055  zeroofn  18056  yonedainv  18347  fn0g  18731  smndex1igid  18975  smndex1igidOLD  18976  smndex1n0mnd  18984  grpinvfn  19058  cycsubmel  19281  conjnmz  19332  ghmquskerco  19364  psgnfn  19581  odf  19617  sylow1lem4  19681  pgpssslw  19694  sylow2blem3  19702  sylow3lem2  19708  cygctb  19972  dprd2da  20124  fnmgp  20228  zrinitorngc  20756  zrtermorngc  20757  zrtermoringc  20789  rrgsupp  20815  rlmfn  21326  frlmup4  21966  asclfn  22045  evlslem1  22248  evlsvvval  22259  psdmplcl  22340  psdadd  22341  psdmul  22344  psdmvr  22347  mdetrlin  22774  fncld  23194  hauseqlcld  23818  kqf  23919  filunirn  24054  fmf  24117  txflf  24178  clsnsg  24282  tgpconncomp  24285  qustgpopn  24292  qustgplem  24293  ustfn  24374  xmetunirn  24509  met1stc  24693  rrxmvallem  25578  ovolf  25656  vitali  25787  i1fmulc  25877  mbfi1fseqlem4  25892  itg2seq  25916  itg2monolem1  25924  i1fibl  25982  fncpn  26107  lhop1lem  26187  mdegxrf  26240  aannenlem3  26508  efabl  26730  logccv  26843  gausslemma2dlem1  27545  padicabvf  27810  mpteleeOLD  29260  wlkiswwlks2lem1  30233  clwlkclwwlklem2a2  30359  grpoinvf  30899  occllem  31670  pjfni  32068  pjmfn  32082  rnbra  32474  bra11  32475  kbass2  32484  hmopidmchi  32518  xppreima2  33011  abfmpunirn  33012  psgnfzto1stlem  33433  elrspunidl  33749  locfinreflem  34243  zarclsint  34275  zar0ring  34281  rhmpreimacn  34288  ofcfn  34503  sxbrsigalem3  34675  eulerpartgbij  34775  sseqfv1  34792  sseqfn  34793  sseqf  34795  sseqfv2  34797  signstlen  34967  kardfn  35576  vonf1oonfo  35611  msubrn  36033  msrf  36046  faclimlem1  36247  weiunlem  37006  bj-evalfn  37747  bj-inftyexpitaufo  37878  matunitlindflem1  38299  poimirlem30  38333  mblfinlem2  38341  volsupnfl  38348  cnambfre  38351  itg2addnclem2  38355  itg2addnclem3  38356  ftc1anclem5  38380  ftc1anclem7  38382  sdclem2  38425  prdsbnd2  38478  rrncmslem  38515  diafn  41840  cdlemm10N  41924  dibfna  41960  lcfrlem9  42356  mapd1o  42454  hdmapfnN  42635  hgmapfnN  42694  fsuppind  43354  rmxypairf1o  43670  hbtlem6  43888  dgraaf  43906  cytpfn  43960  tfsconcatrev  44107  ntrf  44881  uzmptshftfval  45088  binomcxplemrat  45092  addrfn  45212  subrfn  45213  mulvfn  45214  limsup10exlem  46518  liminfvalxr  46529  fourierdlem62  46914  fourierdlem70  46922  fourierdlem71  46923  cjnpoly  47658  fmtnorn  48318  tposideq  49698  cicfn  49852  fucofn22  50150  fucoid  50158  dfinito4  50311  crosspalti  50679