Theorem fnmpti 6641

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∀wral 3051  Vcvv 3429   ↦ cmpt 5166   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  dmmpti  6642  fconst  6726  dffn5  6898  idref  7099  eufnfv  7184  offn  7644  caofinvl  7663  fo1st  7962  fo2nd  7963  reldm  7997  fimaproj  8085  mapsnf1o2  8842  unfilem2  9216  fidomdm  9244  noinfep  9581  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  aceq3lem  10042  dfac4  10044  ackbij2lem2  10161  cfslb2n  10190  axcc2lem  10358  dmct  10446  konigthlem  10491  rankcf  10700  tskuni  10706  seqf1o  14005  ccatlen  14537  ccatvalfn  14543  swrdlen  14610  swrdwrdsymb  14625  swrdswrd  14667  sqrtf  15326  mptfzshft  15740  efcvgfsum  16051  prmreclem2  16888  1arith  16898  vdwlem6  16957  vdwlem8  16959  slotfn  17154  topnfn  17388  fnmre  17553  cidffn  17644  cidfn  17645  funcres  17863  initofn  17954  termofn  17955  zeroofn  17956  yonedainv  18247  fn0g  18631  smndex1igid  18874  smndex1igidOLD  18875  smndex1n0mnd  18883  grpinvfn  18957  cycsubmel  19175  conjnmz  19227  ghmquskerco  19259  psgnfn  19476  odf  19512  sylow1lem4  19576  pgpssslw  19589  sylow2blem3  19597  sylow3lem2  19603  cygctb  19867  dprd2da  20019  fnmgp  20123  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  rrgsupp  20678  rlmfn  21185  frlmup4  21781  asclfn  21860  evlslem1  22060  evlsvvval  22071  psdmplcl  22128  psdadd  22129  psdmul  22132  psdmvr  22135  mdetrlin  22567  fncld  22987  hauseqlcld  23611  kqf  23712  filunirn  23847  fmf  23910  txflf  23971  clsnsg  24075  tgpconncomp  24078  qustgpopn  24085  qustgplem  24086  ustfn  24167  xmetunirn  24302  met1stc  24486  rrxmvallem  25371  ovolf  25449  vitali  25580  i1fmulc  25670  mbfi1fseqlem4  25685  itg2seq  25709  itg2monolem1  25717  i1fibl  25775  fncpn  25900  lhop1lem  25980  mdegxrf  26033  aannenlem3  26296  efabl  26514  logccv  26627  gausslemma2dlem1  27329  padicabvf  27594  mpteleeOLD  28964  wlkiswwlks2lem1  29937  clwlkclwwlklem2a2  30063  grpoinvf  30603  occllem  31374  pjfni  31772  pjmfn  31786  rnbra  32178  bra11  32179  kbass2  32188  hmopidmchi  32222  xppreima2  32724  abfmpunirn  32725  psgnfzto1stlem  33161  elrspunidl  33488  locfinreflem  33984  zarclsint  34016  zar0ring  34022  rhmpreimacn  34029  ofcfn  34244  sxbrsigalem3  34416  eulerpartgbij  34516  sseqfv1  34533  sseqfn  34534  sseqf  34536  sseqfv2  34538  signstlen  34711  msubrn  35711  msrf  35724  faclimlem1  35925  weiunlem  36645  bj-evalfn  37385  bj-inftyexpitaufo  37516  matunitlindflem1  37937  poimirlem30  37971  mblfinlem2  37979  volsupnfl  37986  cnambfre  37989  itg2addnclem2  37993  itg2addnclem3  37994  ftc1anclem5  38018  ftc1anclem7  38020  sdclem2  38063  prdsbnd2  38116  rrncmslem  38153  diafn  41480  cdlemm10N  41564  dibfna  41600  lcfrlem9  41996  mapd1o  42094  hdmapfnN  42275  hgmapfnN  42334  fsuppind  43023  rmxypairf1o  43339  hbtlem6  43557  dgraaf  43575  cytpfn  43629  tfsconcatrev  43776  ntrf  44550  uzmptshftfval  44773  binomcxplemrat  44777  addrfn  44898  subrfn  44899  mulvfn  44900  limsup10exlem  46200  liminfvalxr  46211  fourierdlem62  46596  fourierdlem70  46604  fourierdlem71  46605  nthrucw  47316  cjnpoly  47337  fmtnorn  47997  tposideq  49363  cicfn  49517  fucofn22  49815  fucoid  49823  dfinito4  49976