MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  offval2 Unicode version

Theorem offval2 6556
Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1
offval2.2
offval2.3
offval2.4
offval2.5
Assertion
Ref Expression
offval2
Distinct variable groups:   ,   ,   ,

Proof of Theorem offval2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6
21ralrimiva 2871 . . . . 5
3 eqid 2457 . . . . . 6
43fnmpt 5712 . . . . 5
52, 4syl 16 . . . 4
6 offval2.4 . . . . 5
76fneq1d 5676 . . . 4
85, 7mpbird 232 . . 3
9 offval2.3 . . . . . 6
109ralrimiva 2871 . . . . 5
11 eqid 2457 . . . . . 6
1211fnmpt 5712 . . . . 5
1310, 12syl 16 . . . 4
14 offval2.5 . . . . 5
1514fneq1d 5676 . . . 4
1613, 15mpbird 232 . . 3
17 offval2.1 . . 3
18 inidm 3706 . . 3
196adantr 465 . . . 4
2019fveq1d 5873 . . 3
2114adantr 465 . . . 4
2221fveq1d 5873 . . 3
238, 16, 17, 17, 18, 20, 22offval 6547 . 2
24 nffvmpt1 5879 . . . . 5
25 nfcv 2619 . . . . 5
26 nffvmpt1 5879 . . . . 5
2724, 25, 26nfov 6322 . . . 4
28 nfcv 2619 . . . 4
29 fveq2 5871 . . . . 5
30 fveq2 5871 . . . . 5
3129, 30oveq12d 6314 . . . 4
3227, 28, 31cbvmpt 4542 . . 3
33 simpr 461 . . . . . 6
343fvmpt2 5963 . . . . . 6
3533, 1, 34syl2anc 661 . . . . 5
3611fvmpt2 5963 . . . . . 6
3733, 9, 36syl2anc 661 . . . . 5
3835, 37oveq12d 6314 . . . 4
3938mpteq2dva 4538 . . 3
4032, 39syl5eq 2510 . 2
4123, 40eqtrd 2498 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  e.cmpt 4510  Fnwfn 5588  `cfv 5593  (class class class)co 6296  oFcof 6538
This theorem is referenced by:  ofmpteq  6558  ofc12  6565  caofinvl  6567  caofcom  6572  caofass  6574  caofdi  6576  caofdir  6577  caonncan  6578  offval22  6879  o1add2  13446  o1mul2  13447  o1sub2  13448  o1dif  13452  fsumo1  13626  pwsplusgval  14887  pwsmulrval  14888  pwsvscafval  14891  pwsco1mhm  16001  pwsco2mhm  16002  pwssub  16183  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsummptfsadd  16940  gsummptfsaddOLD  16941  gsummptfidmadd2  16943  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsub  16974  gsumsubOLD  16975  gsummptfssub  16976  dprdfadd  17060  dprdfsub  17061  dprdfeq0  17062  dprdf11  17063  dprdfaddOLD  17067  dprdfsubOLD  17068  dprdfeq0OLD  17069  dprdf11OLD  17070  lmhmvsca  17691  rrgsupp  17939  rrgsuppOLD  17940  psrbagaddcl  18020  psrbagaddclOLD  18021  psrass1lem  18029  psrlinv  18050  psrass1  18060  psrdi  18061  psrdir  18062  psrass23l  18063  psrcom  18064  psrass23  18065  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplmon2  18158  evlslem1  18184  coe1sclmul  18323  coe1sclmul2  18325  uvcresum  18824  grpvrinv  18898  mhmvlin  18899  mamudi  18905  mamudir  18906  mdetunilem9  19122  tsmssub  20651  tgptsmscls  20652  tsmssplit  20654  tsmsxplem2  20656  ovolctb  21901  mbfmulc2re  22055  mbfneg  22057  mbfadd  22068  mbfsub  22069  mbfmulc2  22070  mbfmul  22133  itg2const  22147  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2monolem1  22157  i1fibl  22214  itgitg1  22215  ibladdlem  22226  ibladd  22227  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  dvmulf  22346  dvcmulf  22348  dvcof  22351  dvexp  22356  dvmptadd  22363  dvmptmul  22364  dvmptco  22375  dvef  22381  dv11cn  22402  itgsubstlem  22449  mdegmullem  22478  plypf1  22609  plyaddlem1  22610  plymullem1  22611  plyco  22638  dgrcolem1  22670  dgrcolem2  22671  plydiveu  22694  plyremlem  22700  elqaalem3  22717  iaa  22721  taylply2  22763  ulmdvlem1  22795  iblulm  22802  jensenlem2  23317  amgmlem  23319  ftalem7  23352  basellem8  23361  basellem9  23362  dchrmulid2  23527  dchrinvcl  23528  dchrfi  23530  lgseisenlem3  23626  lgseisenlem4  23627  chtppilimlem2  23659  chebbnd2  23662  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  vmadivsum  23667  rpvmasumlem  23672  mudivsum  23715  selberglem1  23730  selberglem2  23731  selberg2lem  23735  selberg2  23736  pntrsumo1  23750  selbergr  23753  ofoprabco  27505  pl1cn  27937  esumadd  28064  ofccat  28497  ofs1  28499  itg2addnclem  30066  itg2addnclem3  30068  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nclem1  30081  itgmulc2nclem2  30082  itgmulc2nc  30083  itgabsnc  30084  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  mendlmod  31142  mendassa  31143  expgrowthi  31238  expgrowth  31240  binomcxplemrat  31255  mulcncff  31670  subcncff  31682  addcncff  31687  divcncff  31694  dvsubf  31709  dvdivf  31719  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem58  31947  fourierdlem59  31948  fourierdlem72  31961  fourierdlem83  31972  offvalfv  32932  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6540
  Copyright terms: Public domain W3C validator