Theorem fnmpti 6463

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ↦ cmpt 5110   Fn wfn 6319

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6326  df-fn 6327

This theorem is referenced by:  dmmpti  6464  fconst  6539  dffn5  6699  idref  6885  eufnfv  6969  offn  7400  caofinvl  7416  fo1st  7691  fo2nd  7692  reldm  7725  fimaproj  7812  mapsnf1o2  8441  unfilem2  8767  fidomdm  8785  pwfilem  8802  noinfep  9107  aceq3lem  9531  dfac4  9533  ackbij2lem2  9651  cfslb2n  9679  axcc2lem  9847  dmct  9935  konigthlem  9979  rankcf  10188  tskuni  10194  seqf1o  13407  ccatlen  13918  ccatlenOLD  13919  ccatvalfn  13926  swrdlen  14000  swrdwrdsymb  14015  swrdswrd  14058  sqrtf  14715  mptfzshft  15125  fprodrev  15323  efcvgfsum  15431  prmreclem2  16243  1arith  16253  vdwlem6  16312  vdwlem8  16314  slotfn  16493  topnfn  16691  fnmre  16854  cidffn  16941  cidfn  16942  funcres  17158  yonedainv  17523  fn0g  17865  smndex1igid  18061  smndex1n0mnd  18069  grpinvfn  18137  cycsubmel  18335  conjnmz  18384  psgnfn  18621  odf  18657  sylow1lem4  18718  pgpssslw  18731  sylow2blem3  18739  sylow3lem2  18745  cygctb  19005  dprd2da  19157  fnmgp  19234  rlmfn  19955  rrgsupp  20057  frlmup4  20490  asclfn  20567  evlslem1  20754  mdetrlin  21207  fncld  21627  hauseqlcld  22251  kqf  22352  filunirn  22487  fmf  22550  txflf  22611  clsnsg  22715  tgpconncomp  22718  qustgpopn  22725  qustgplem  22726  ustfn  22807  xmetunirn  22944  met1stc  23128  rrxmvallem  24008  ovolf  24086  vitali  24217  i1fmulc  24307  mbfi1fseqlem4  24322  itg2seq  24346  itg2monolem1  24354  i1fibl  24411  fncpn  24536  lhop1lem  24616  mdegxrf  24669  aannenlem3  24926  efabl  25142  logccv  25254  gausslemma2dlem1  25950  padicabvf  26215  mptelee  26689  wlkiswwlks2lem1  27655  clwlkclwwlklem2a2  27778  grpoinvf  28315  occllem  29086  pjfni  29484  pjmfn  29498  rnbra  29890  bra11  29891  kbass2  29900  hmopidmchi  29934  xppreima2  30413  abfmpunirn  30415  psgnfzto1stlem  30792  elrspunidl  31014  locfinreflem  31193  zarclsint  31225  zar0ring  31231  rhmpreimacn  31238  ofcfn  31469  sxbrsigalem3  31640  eulerpartgbij  31740  sseqfv1  31757  sseqfn  31758  sseqf  31760  sseqfv2  31762  signstlen  31947  msubrn  32889  msrf  32902  faclimlem1  33088  bj-evalfn  34489  bj-inftyexpitaufo  34617  matunitlindflem1  35053  poimirlem30  35087  mblfinlem2  35095  volsupnfl  35102  cnambfre  35105  itg2addnclem2  35109  itg2addnclem3  35110  ftc1anclem5  35134  ftc1anclem7  35136  sdclem2  35180  prdsbnd2  35233  rrncmslem  35270  diafn  38330  cdlemm10N  38414  dibfna  38450  lcfrlem9  38846  mapd1o  38944  hdmapfnN  39125  hgmapfnN  39184  fsuppind  39456  rmxypairf1o  39852  hbtlem6  40073  dgraaf  40091  cytpfn  40152  ntrf  40826  uzmptshftfval  41050  binomcxplemrat  41054  addrfn  41176  subrfn  41177  mulvfn  41178  limsup10exlem  42414  liminfvalxr  42425  fourierdlem62  42810  fourierdlem70  42818  fourierdlem71  42819  fmtnorn  44051  zrinitorngc  44624  zrtermorngc  44625  zrtermoringc  44694