Theorem fnmpti 6572

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

Syntax hints:   = wceq 1541   ∈ wcel 2109  ∀wral 3065  Vcvv 3430   ↦ cmpt 5161   Fn wfn 6425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-fun 6432  df-fn 6433

This theorem is referenced by:  dmmpti  6573  fconst  6656  dffn5  6822  idref  7012  eufnfv  7099  offn  7537  caofinvl  7554  fo1st  7837  fo2nd  7838  reldm  7871  fimaproj  7960  mapsnf1o2  8656  unfilem2  9040  fidomdm  9057  pwfilemOLD  9074  noinfep  9379  ssttrcl  9434  ttrcltr  9435  ttrclselem2  9445  aceq3lem  9860  dfac4  9862  ackbij2lem2  9980  cfslb2n  10008  axcc2lem  10176  dmct  10264  konigthlem  10308  rankcf  10517  tskuni  10523  seqf1o  13745  ccatlen  14259  ccatlenOLD  14260  ccatvalfn  14267  swrdlen  14341  swrdwrdsymb  14356  swrdswrd  14399  sqrtf  15056  mptfzshft  15471  efcvgfsum  15776  prmreclem2  16599  1arith  16609  vdwlem6  16668  vdwlem8  16670  slotfn  16866  topnfn  17117  fnmre  17281  cidffn  17368  cidfn  17369  funcres  17592  initofn  17683  termofn  17684  zeroofn  17685  yonedainv  17980  fn0g  18328  smndex1igid  18524  smndex1n0mnd  18532  grpinvfn  18602  cycsubmel  18800  conjnmz  18849  psgnfn  19090  odf  19126  sylow1lem4  19187  pgpssslw  19200  sylow2blem3  19208  sylow3lem2  19214  cygctb  19474  dprd2da  19626  fnmgp  19703  rlmfn  20441  rrgsupp  20543  frlmup4  20989  asclfn  21066  evlslem1  21273  mdetrlin  21732  fncld  22154  hauseqlcld  22778  kqf  22879  filunirn  23014  fmf  23077  txflf  23138  clsnsg  23242  tgpconncomp  23245  qustgpopn  23252  qustgplem  23253  ustfn  23334  xmetunirn  23471  met1stc  23658  rrxmvallem  24549  ovolf  24627  vitali  24758  i1fmulc  24849  mbfi1fseqlem4  24864  itg2seq  24888  itg2monolem1  24896  i1fibl  24953  fncpn  25078  lhop1lem  25158  mdegxrf  25214  aannenlem3  25471  efabl  25687  logccv  25799  gausslemma2dlem1  26495  padicabvf  26760  mptelee  27244  wlkiswwlks2lem1  28213  clwlkclwwlklem2a2  28336  grpoinvf  28873  occllem  29644  pjfni  30042  pjmfn  30056  rnbra  30448  bra11  30449  kbass2  30458  hmopidmchi  30492  xppreima2  30967  abfmpunirn  30968  psgnfzto1stlem  31346  elrspunidl  31585  locfinreflem  31769  zarclsint  31801  zar0ring  31807  rhmpreimacn  31814  ofcfn  32047  sxbrsigalem3  32218  eulerpartgbij  32318  sseqfv1  32335  sseqfn  32336  sseqf  32338  sseqfv2  32340  signstlen  32525  msubrn  33470  msrf  33483  faclimlem1  33688  bj-evalfn  35224  bj-inftyexpitaufo  35352  matunitlindflem1  35752  poimirlem30  35786  mblfinlem2  35794  volsupnfl  35801  cnambfre  35804  itg2addnclem2  35808  itg2addnclem3  35809  ftc1anclem5  35833  ftc1anclem7  35835  sdclem2  35879  prdsbnd2  35932  rrncmslem  35969  diafn  39027  cdlemm10N  39111  dibfna  39147  lcfrlem9  39543  mapd1o  39641  hdmapfnN  39822  hgmapfnN  39881  evlsbagval  40255  fsuppind  40259  mhphf  40265  rmxypairf1o  40713  hbtlem6  40934  dgraaf  40952  cytpfn  41013  ntrf  41686  uzmptshftfval  41917  binomcxplemrat  41921  addrfn  42043  subrfn  42044  mulvfn  42045  limsup10exlem  43267  liminfvalxr  43278  fourierdlem62  43663  fourierdlem70  43671  fourierdlem71  43672  fmtnorn  44938  zrinitorngc  45510  zrtermorngc  45511  zrtermoringc  45580