Theorem fnmpti 6494

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

Syntax hints:   = wceq 1536   ∈ wcel 2113  ∀wral 3141  Vcvv 3497   ↦ cmpt 5149   Fn wfn 6353

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-fun 6360  df-fn 6361

This theorem is referenced by:  dmmpti  6495  fconst  6568  dffn5  6727  idref  6911  eufnfv  6994  offn  7423  caofinvl  7439  fo1st  7712  fo2nd  7713  reldm  7746  fimaproj  7832  mapsnf1o2  8461  unfilem2  8786  fidomdm  8804  pwfilem  8821  noinfep  9126  aceq3lem  9549  dfac4  9551  ackbij2lem2  9665  cfslb2n  9693  axcc2lem  9861  dmct  9949  konigthlem  9993  rankcf  10202  tskuni  10208  seqf1o  13414  ccatlen  13930  ccatlenOLD  13931  ccatvalfn  13938  swrdlen  14012  swrdwrdsymb  14027  swrdswrd  14070  sqrtf  14726  mptfzshft  15136  fprodrev  15334  efcvgfsum  15442  prmreclem2  16256  1arith  16266  vdwlem6  16325  vdwlem8  16327  slotfn  16504  topnfn  16702  fnmre  16865  cidffn  16952  cidfn  16953  funcres  17169  yonedainv  17534  fn0g  17876  smndex1igid  18072  smndex1n0mnd  18080  grpinvfn  18148  cycsubmel  18346  conjnmz  18395  psgnfn  18632  odf  18668  sylow1lem4  18729  pgpssslw  18742  sylow2blem3  18750  sylow3lem2  18756  cygctb  19015  dprd2da  19167  fnmgp  19244  rlmfn  19965  rrgsupp  20067  asclfn  20113  evlslem1  20298  frlmup4  20948  mdetrlin  21214  fncld  21633  hauseqlcld  22257  kqf  22358  filunirn  22493  fmf  22556  txflf  22617  clsnsg  22721  tgpconncomp  22724  qustgpopn  22731  qustgplem  22732  ustfn  22813  xmetunirn  22950  met1stc  23134  rrxmvallem  24010  ovolf  24086  vitali  24217  i1fmulc  24307  mbfi1fseqlem4  24322  itg2seq  24346  itg2monolem1  24354  i1fibl  24411  fncpn  24533  lhop1lem  24613  mdegxrf  24665  aannenlem3  24922  efabl  25137  logccv  25249  gausslemma2dlem1  25945  padicabvf  26210  mptelee  26684  wlkiswwlks2lem1  27650  clwlkclwwlklem2a2  27774  grpoinvf  28312  occllem  29083  pjfni  29481  pjmfn  29495  rnbra  29887  bra11  29888  kbass2  29897  hmopidmchi  29931  xppreima2  30398  abfmpunirn  30400  psgnfzto1stlem  30746  locfinreflem  31108  ofcfn  31363  sxbrsigalem3  31534  eulerpartgbij  31634  sseqfv1  31651  sseqfn  31652  sseqf  31654  sseqfv2  31656  signstlen  31841  msubrn  32780  msrf  32793  faclimlem1  32979  bj-evalfn  34369  bj-inftyexpitaufo  34488  matunitlindflem1  34892  poimirlem30  34926  mblfinlem2  34934  volsupnfl  34941  cnambfre  34944  itg2addnclem2  34948  itg2addnclem3  34949  ftc1anclem5  34975  ftc1anclem7  34977  sdclem2  35021  prdsbnd2  35077  rrncmslem  35114  diafn  38174  cdlemm10N  38258  dibfna  38294  lcfrlem9  38690  mapd1o  38788  hdmapfnN  38969  hgmapfnN  39028  rmxypairf1o  39514  hbtlem6  39735  dgraaf  39753  cytpfn  39814  ntrf  40479  uzmptshftfval  40684  binomcxplemrat  40688  addrfn  40810  subrfn  40811  mulvfn  40812  limsup10exlem  42059  liminfvalxr  42070  fourierdlem62  42460  fourierdlem70  42468  fourierdlem71  42469  fmtnorn  43703  zrinitorngc  44278  zrtermorngc  44279  zrtermoringc  44348