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

Theorem eqidd 2284
Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
Assertion
Ref Expression
eqidd  |-  ( ph  ->  A  =  A )

Proof of Theorem eqidd
StepHypRef Expression
1 eqid 2283 . 2  |-  A  =  A
21a1i 10 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  nfabd2  2437  cbvraldva  2770  cbvrexdva  2771  opeq1  3796  opeq2  3797  mpteq1  4100  nfcvb  4205  tfisi  4649  iotanul  5234  feq23d  5386  fvmptdv2  5613  fmptco  5691  fliftfun  5811  fliftval  5815  cbvmpt2  5925  eqfnov2  5951  ovmpt2d  5975  ovmpt2dv2  5981  ofval  6087  ofrval  6088  offn  6089  fnfvof  6090  off  6093  ofres  6094  ofco  6097  caofref  6103  caofid0l  6105  caofid0r  6106  caofid1  6107  caofid2  6108  caofrss  6110  caoftrn  6112  suppssof1  6119  riotabidv  6306  nfriotad  6313  iserd  6686  ixpsnf1o  6856  mapxpen  7027  dffi3  7184  oieq1  7227  oieq2  7228  cantnfp1  7383  cantnflem1d  7390  cantnflem1  7391  iunfictbso  7741  axcclem  8083  ttukeylem3  8138  ttukey2g  8143  fpwwe2lem9  8260  wunex2  8360  wuncval2  8369  ofsubeq0  9743  ofnegsub  9744  ofsubge0  9745  seqeq2  11050  seqeq3  11051  seqid  11091  seqid2  11092  seqz  11094  seqof  11103  bcval  11317  swrdval  11450  wrdind  11477  revco  11489  ccatco  11490  rlim2  11970  climcl  11973  rlimcl  11977  clim2  11978  lo1o12  12007  rlimclim1  12019  rlimclim  12020  climrlim2  12021  climuni  12026  rlimres  12032  climeq  12041  2clim  12046  climshftlem  12048  climabs0  12059  rlimcn1b  12063  climcn1  12065  climcn2  12066  o1of2  12086  o1rlimmul  12092  o1add2  12097  o1mul2  12098  o1sub2  12099  o1dif  12103  climsqz  12114  climsqz2  12115  rlimdiv  12119  isercoll  12141  climsup  12143  climcau  12144  caurcvgr  12146  caucvgb  12152  serf0  12153  iseralt  12157  cbvsum  12168  summolem2a  12188  zsum  12191  fsum  12193  sumz  12195  sumss  12197  fsumss  12198  sumss2  12199  fsumcvg2  12200  fsumser  12203  isumclim3  12222  isummulc2  12225  fsum2dlem  12233  fsumconst  12252  fsumabs  12259  fsumparts  12264  fsumrlim  12269  fsumo1  12270  seqabs  12272  cvgcmpce  12276  fsumiun  12279  ackbijnn  12286  isumshft  12298  isumless  12304  isumltss  12307  climcndslem1  12308  climcndslem2  12309  climcnds  12310  mertenslem1  12340  mertenslem2  12341  eftlcl  12387  reeftlcl  12388  eftlub  12389  efsep  12390  effsumlt  12391  eirrlem  12482  rpnnen2lem1  12493  rpnnen2lem6  12498  rpnnen2lem7  12499  rpnnen2lem8  12500  rpnnen2lem9  12501  rpnnen2  12504  rpnnen  12505  bitsp1  12622  sadadd2lem  12650  sadadd2  12651  sadasslem  12661  smupvallem  12674  smumul  12684  alginv  12745  algfx  12750  qnumdencoprm  12816  qeqnumdivden  12817  pcmpt  12940  pcmptdvds  12942  prmreclem2  12964  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  prmrec  12969  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  ramub1lem2  13074  ramcl  13076  prdssca  13356  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsle  13361  prdsds  13363  prdstset  13365  prdshom  13366  prdsco  13367  prdsvscafval  13379  prdsdsval2  13383  prdsdsval3  13384  pwsle  13391  pwsleval  13392  pwsvscaval  13394  imasbas  13415  imasds  13416  imasplusg  13420  imasmulr  13421  imassca  13422  imasvsca  13423  imastset  13424  imasle  13425  imasvscafn  13439  imasvscaval  13440  divsin  13446  xpsvsca  13481  mrcfval  13510  iscat  13574  iscatd  13575  catidex  13576  cidval  13579  catidd  13582  iscatd2  13583  catlid  13585  catrid  13586  0catg  13589  homfeq  13597  homfeqd  13598  comfffval2  13604  comffval2  13605  comfeq  13609  comfeqd  13610  oppccatid  13622  2oppccomf  13628  ismon  13636  moni  13639  ssc2  13699  ssctr  13702  ssceq  13703  subcssc  13714  subccat  13722  subsubc  13727  isfunc  13738  funcres  13770  funcres2  13772  funcres2c  13775  idffth  13807  cofull  13808  cofth  13809  ressffth  13812  isnat  13821  fuccofval  13833  fucco  13836  fuccatid  13843  fucpropd  13851  elhomai  13865  coafval  13896  setcval  13909  setcbas  13910  setchomfval  13911  setccofval  13914  setcco  13915  setccatid  13916  setcepi  13920  funcsetcres2  13925  catcval  13928  catcbas  13929  catchomfval  13930  catccofval  13932  catcco  13933  catccatid  13934  catciso  13939  catcfuccl  13941  xpcbas  13952  xpchomfval  13953  xpccofval  13956  xpccatid  13962  1stfcl  13971  2ndfcl  13972  prfval  13973  catcxpccl  13981  xpcpropd  13982  evlfval  13991  curfval  13997  curf1  13999  curf12  14001  curf2  14003  curf2val  14004  curfpropd  14007  hofval  14026  hof2fval  14029  hofcllem  14032  oppchofcl  14034  oppcyon  14043  oyoncl  14044  yonedalem4a  14049  yonedalem4b  14050  yonedalem4c  14051  yonedalem3b  14053  yonedainv  14055  oduposb  14240  ipopos  14263  isdlat  14296  ismnd  14369  ismndd  14396  mndprop  14400  prdsmndd  14405  imasmnd2  14409  gsumpropd  14453  gsumval1  14456  gsumval2a  14459  frmdbas  14474  frmdmnd  14481  grpprop  14501  grpsubfval  14524  grpsubpropd  14566  mulgfval  14568  mulgpropd  14600  prdsgrpd  14604  imasgrp2  14610  imasgrp  14611  imasgrpf1  14612  subgsub  14633  eqgfval  14665  divsgrp  14672  symgval  14771  symggrp  14780  oppgmnd  14827  oppgmndb  14828  oppggrp  14830  oppggrpb  14831  odfval  14848  oppglsm  14953  lsmelvalmi  14963  efgi0  15029  efgi1  15030  efgtf  15031  efgval2  15033  efginvrel2  15036  frgp0  15069  frgpup3lem  15086  ablprop  15100  subcmn  15133  gex2abl  15143  prdscmnd  15153  divsabl  15157  cyggenod2  15172  cygabl  15177  gsumzf1o  15196  gsumzaddlem  15203  gsumzsplit  15206  gsumconst  15209  gsummhm2  15212  gsumunsn  15221  gsumpt  15222  gsum2d  15223  gsumcom2  15226  dprdval  15238  dprdssv  15251  dprdfeq0  15257  dprdsubg  15259  dprdspan  15262  dprdz  15265  subgdmdprd  15269  subgdprd  15270  dmdprdsplitlem  15272  dprd2d2  15279  isrng  15345  rngabl  15370  rngprop  15374  isrngd  15375  prdsrngd  15395  prdscrngd  15396  prds1  15397  imasrng  15402  opprrng  15413  opprrngb  15414  dvrfval  15466  pwsco1rhm  15510  pwsco2rhm  15511  drngprop  15523  isdrngd  15537  isdrngrd  15538  pwsdiagrhm  15578  abvtrivd  15605  islmodd  15633  lmodabl  15672  lss1  15696  lsssn0  15705  islss3  15716  lss1d  15720  lssintcl  15721  prdslmodd  15726  idlmhm  15798  invlmhm  15799  lmhmvsca  15802  lbsextlem2  15912  sralmod  15939  sralmod0  15940  rlm0  15950  rlmvneg  15959  crngridl  15990  divscrng  15992  isassa  16056  isassad  16063  issubassa  16064  sraassa  16065  asclfval  16074  ressascl  16083  psrval  16110  psrbaglesupp  16114  psrbagcon  16117  psrbaglefi  16118  psrbagconf1o  16120  gsumbagdiaglem  16121  psrass1lem  16123  psrbas  16124  psrplusg  16126  psrmulr  16129  psrsca  16134  psrvscafval  16135  psrvscaval  16137  psrgrp  16143  psrlmod  16146  psrlidm  16148  psrdi  16151  psrdir  16152  psrcom  16153  psrrng  16155  psrassa  16158  mplsubglem  16179  mpllsslem  16180  mplvscaval  16192  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  opsrcrng  16229  opsrassa  16230  mplmon2  16234  evlslem2  16249  ply1lss  16275  ply1subrg  16276  opsr0  16295  opsr1  16296  subrgply1  16311  psrplusgpropd  16313  psropprmul  16316  opsrrng  16323  opsrlmod  16324  ply1mpl0  16333  ply1mpl1  16334  coe1z  16340  coe1mul2  16346  coe1tm  16349  coe1tmmul2fv  16354  coe1pwmulfv  16356  coe1sclmulfv  16359  ply1coe  16368  absabv  16429  zrhpropd  16469  znzrh  16496  znbas  16497  zncrng  16498  znzrhfo  16501  znf1o  16505  cyggic  16526  frgpcyg  16527  isphld  16558  phlpropd  16559  pjfval  16606  epttop  16746  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  lmss  17026  2ndci  17174  2ndcsep  17185  dis2ndc  17186  1stcelcls  17187  ptbasid  17270  xkoopn  17284  prdstopn  17322  ptrescn  17333  txlm  17342  lmcn2  17343  tx1stc  17344  xkopt  17349  cnmpt2c  17364  cnmptk1  17375  cnmpt1k  17376  cnmptkk  17377  qtopeu  17407  txswaphmeolem  17495  xpstopnlem1  17500  ptcmpfi  17504  xkohmeo  17506  rnelfmlem  17647  rnelfm  17648  hauspwpwf1  17682  lmflf  17700  flfcnp2  17702  fclsval  17703  alexsubb  17740  tmdgsum  17778  tgpconcomp  17795  divstgphaus  17805  tsmsfbas  17810  tsmspropd  17814  tsms0  17824  tsmsmhm  17828  tgptsmscls  17832  tsmssplit  17834  tsmsxplem1  17835  tsmsxplem2  17836  imasdsf1olem  17937  blfval  17947  stdbdmetval  18060  stdbdxmet  18061  met2ndci  18068  prdsxmslem2  18075  nmfval  18111  nmpropd  18116  nmpropd2  18117  subgnm  18149  tng0  18159  tngnm  18167  tngnrg  18185  sranlm  18195  qdensere  18279  fsumcn  18374  cncfmpt1f  18417  negfcncf  18422  oprpiece1res2  18450  htpyid  18475  phtpyid  18487  pcofval  18508  pcopt2  18521  om1bas  18529  om1plusg  18532  om1tset  18533  pi1bas  18536  pi1bas2  18539  pi1eluni  18540  pi1bas3  18541  pi1cpbl  18542  pi1addf  18545  pi1addval  18546  pi1grplem  18547  pi1xfr  18553  pi1xfrcnvlem  18554  pi1coghm  18559  cphassr  18647  tchphl  18658  ipcau2  18664  lmnn  18689  iscau  18702  cmetcaulem  18714  iscmet3lem1  18717  causs  18724  lmclim  18728  srabn  18777  ovollb2lem  18847  ovolfiniun  18860  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  shftmbl  18896  volfiniun  18904  ioombl1lem4  18918  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  vitalilem4  18966  ismbfcn2  18994  mbfmulc2lem  19002  mbfmulc2re  19003  mbfneg  19005  mbfposb  19008  mbfaddlem  19015  mbfadd  19016  mbfsub  19017  mbfmulc2  19018  0plef  19027  0pledm  19028  itg1ge0  19041  i1faddlem  19048  i1fmullem  19049  i1fmulclem  19057  itg1mulc  19059  i1fres  19060  i1fposd  19062  itg1lea  19067  itg1le  19068  itg1climres  19069  mbfi1fseqlem2  19071  mbfi1fseq  19076  mbfi1flimlem  19077  mbfi1flim  19078  mbfmullem2  19079  mbfmul  19081  xrge0f  19086  itg2ge0  19090  itg2const  19095  itg2const2  19096  itg2uba  19098  itg2lea  19099  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  isibl  19120  isibl2  19121  iblitg  19123  dfitg  19124  cbvitg  19130  itgeq2  19132  itgcl  19138  itgvallem  19139  ibl0  19141  iblcnlem1  19142  itgcnlem  19144  iblneg  19157  itgneg  19158  iblss  19159  iblss2  19160  i1fibl  19162  itgitg1  19163  itgle  19164  itgeqa  19168  itgss3  19169  iblconst  19172  ibladdlem  19174  ibladd  19175  itgaddlem1  19177  itgfsum  19181  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  itgsplit  19190  bddmulibl  19193  bddibl  19194  itgcn  19197  limccnp  19241  limccnp2  19242  limcco  19243  dvidlem  19265  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvaddf  19291  dvcmulf  19294  dvcobr  19295  dvcjbr  19298  dvexp  19302  dvmptadd  19309  dvmptmul  19310  dvmptcj  19317  dvmptco  19321  dvmptfsum  19322  dvcnvlem  19323  dvef  19327  rolle  19337  mvth  19339  dvlip  19340  dvlipcn  19341  lhop1lem  19360  itgsubstlem  19395  evlslem1  19399  mpfrcl  19402  evlsval  19403  evl1rhm  19412  evl1sca  19413  evl1expd  19421  deg1suble  19493  ply1divalg2  19524  uc1pmon1p  19537  q1pval  19539  r1pval  19542  elply2  19578  elplyr  19583  plypf1  19594  plyaddlem1  19595  coeeulem  19606  plyco  19623  coeaddlem  19630  coemulc  19636  dgradd2  19649  dgrsub  19653  dgrcolem1  19654  dgrcolem2  19655  dgrco  19656  ofmulrt  19662  plydivlem3  19675  plydivlem4  19676  plyrem  19685  iaa  19705  aareccl  19706  aannenlem2  19709  aaliou3lem3  19724  aaliou3lem7  19729  taylfval  19738  taylply2  19747  dvntaylp  19750  taylthlem2  19753  ulmclm  19766  ulmres  19767  ulmshftlem  19768  ulm0  19770  ulmcau  19772  ulmss  19774  ulmbdd  19775  ulmcn  19776  mtest  19781  iblulm  19783  itgulm  19784  pserulm  19798  pserdvlem2  19804  abelthlem5  19811  abelthlem6  19812  abelthlem8  19815  abelthlem9  19816  sincn  19820  coscn  19821  efcvx  19825  logfac  19954  logcn  19994  chordthmlem  20129  chordthmlem5  20133  mcubic  20143  leibpi  20238  efrlim  20264  amgmlem  20284  basellem7  20324  basellem9  20326  vmaval  20351  prmorcht  20416  musum  20431  chtublem  20450  pclogsum  20454  logexprlim  20464  dchrbas  20474  dchrelbasd  20478  dchr1cl  20490  dchrabl  20493  dchrfi  20494  dchrptlem2  20504  dchrhash  20510  bposlem5  20527  bposlem6  20528  lgsfval  20540  lgsdir2lem5  20566  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgsquad2lem2  20598  2sqlem8  20611  2sqlem11  20614  chtppilimlem2  20623  chebbnd2  20626  chpchtlim  20628  chpo1ub  20629  vmadivsum  20631  rplogsumlem2  20634  rpvmasumlem  20636  dchrisum0re  20662  dchrisum0  20669  mudivsum  20679  selberglem1  20694  selberglem2  20695  selberg2lem  20699  selberg2  20700  pntrsumo1  20714  selbergr  20717  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  abvcxp  20764  grpodivfval  20909  gxfval  20924  isrngo  21045  dipfval  21275  ipval2  21280  lnoval  21330  ajfval  21387  minvecolem3  21455  h2hcau  21559  h2hlm  21560  opsqrlem3  22722  opsqrlem4  22723  ballotlemsval  23067  ballotlemieq  23075  itgeq12dv  23196  ofrn2  23207  off2  23208  fmptcof2  23229  cofmpt  23231  tpr2rico  23296  disjdifprg  23352  iundisjf  23365  lmdvglim  23377  gsumpropd2lem  23379  gsumconstf  23381  esumeq1  23417  esumeq2d  23419  esumc  23430  esumsplit  23431  esumcst  23436  esumsn  23437  esumpinfval  23441  esumcocn  23448  esummulc1  23449  hasheuni  23453  esumcvg  23454  ofcval  23460  ofcfn  23461  ofcfeqd2  23462  ofcf  23464  ofcfval4  23466  sigaval  23471  issgon  23484  sxval  23521  measvunilem0  23541  measvuni  23542  meascnbl  23546  itgmeq123dTMP  23589  itgmeq1dTMP  23590  itgmeq2dTMP  23591  itgmeq3dTMP  23592  indf1ofs  23609  totprobd  23629  probfinmeasb  23632  probmeasb  23633  orvcval4  23661  dstfrvclim1  23678  quartfull  23686  sconpi1  23770  cvmliftphtlem  23848  cvmlift3lem2  23851  eupath2lem2  23902  sinccvg  24006  circum  24007  relexp0  24025  relexpsucr  24026  rtrclreclem.subset  24042  rtrclreclem.min  24044  dfrtrcl2  24045  br8  24113  br4  24115  trpred0  24239  elno2  24308  brsegle  24731  hilbert1.1  24777  areacirc  24931  eqfnung2  25118  fprg  25133  islatalg  25183  isoriso  25212  fsumprd  25329  fincmpzer  25350  ltrcmp  25405  vecval1b  25451  vecval3b  25452  vri  25492  islimrs  25580  isaddrv  25646  isnullcv  25652  valvze  25654  isucv  25677  ismulcv  25681  fnmulcv  25684  isdivcv2  25693  isder  25707  imonclem  25813  iepiclem  25823  isntr  25873  islimcat  25876  partarelt2  25897  isgraphmrph  25923  domcatfun  25925  domcatval  25930  codcatfun  25934  codcatval  25936  clscnc  26010  cndpv  26049  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  xsyysx  26145  isray  26154  trer  26227  tailfval  26321  unirep  26349  upixp  26403  sdc  26454  lmclim2  26474  geomcau  26475  caures  26476  caushft  26477  prdsbnd2  26519  heibor1lem  26533  bfplem2  26547  rrncmslem  26556  eldiophb  26836  eldioph  26837  eldioph3  26845  rabren3dioph  26898  pellqrexplicit  26962  rmxycomplete  27002  rmxynorm  27003  acongrep  27067  jm2.26a  27093  jm2.26  27095  fnwe2lem2  27148  fnwe2lem3  27149  aomclem5  27155  aomclem8  27159  dsmmval  27200  dsmmsubg  27209  imasgim  27264  isnumbasgrplem1  27266  islindf  27282  islindf4  27308  hbtlem5  27332  dgrsub2  27339  rgspnid  27377  rngunsnply  27378  pmtrval  27394  symgsssg  27408  symgfisg  27409  psgnunilem4  27420  psgnvalii  27432  mamufval  27443  mamuval  27444  mamudi  27461  mamudir  27462  mat0  27472  matinvg  27473  matlmod  27479  matrng  27480  matassa  27481  mdetfval  27487  mendval  27491  mendrng  27500  mendlmod  27501  mendassa  27502  caofcan  27540  ofsubid  27541  ofmul12  27542  ofdivrec  27543  ofdivcan4  27544  ofdivdiv2  27545  expgrowth  27552  fmuldfeqlem1  27712  clim1fr1  27727  climrec  27729  climexp  27731  climinf  27732  climsuse  27734  climneg  27736  stoweidlem2  27751  stoweidlem17  27766  stoweidlem21  27770  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem44  27793  stoweidlem46  27795  stoweidlem55  27804  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem14  27836  afveq12d  27996  afveq1  27997  afveq2  27998  afvco2  28037  rspceaov  28057  ffnaov  28059  faovcl  28060  s2f1o  28091  s4f1o  28093  usgra0v  28117  usgra1v  28126  usgraexvlem  28127  nbgranself  28149  frgra3vlem1  28178  3vfriswmgralem  28182  lflset  29249  islfld  29252  lfladdcl  29261  lflvscl  29267  lkrsc  29287  eqlkr2  29290  lshpkrlem1  29300  ldualset  29315  ldualvaddval  29321  ldualvsval  29328  ldualgrplem  29335  lduallmodlem  29342  cmtfvalN  29400  isoml  29428  iscvlat  29513  llni2  29701  lplni2  29726  lvoli3  29766  lvoli2  29770  paddfval  29986  lhpset  30184  ltrnfset  30306  trlfset  30349  cdleme21k  30527  cdlemeiota  30774  tgrpfset  30933  tgrpset  30934  tgrpabl  30940  tendo0cbv  30975  tendo02  30976  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  cdlemk40  31106  cdlemkid5  31124  cdlemkid  31125  dvafset  31193  dvaset  31194  diaffval  31220  dialss  31236  diaf11N  31239  dvhfset  31270  dvhset  31271  docaffvalN  31311  dibfval  31331  dibf11N  31351  diblss  31360  diclss  31383  dihord2cN  31411  dihord11b  31412  dihffval  31420  dihord6apre  31446  dihglblem2aN  31483  dihglblem2N  31484  dihjatcclem4  31611  lclkrs  31729  mapdh6dN  31929  mapdh6eN  31930  mapdh6fN  31931  mapdh6jN  31935  hvmapffval  31948  hvmapfval  31949  mapdh8a  31965  mapdh8ad  31969  mapdh8d0N  31972  mapdh8d  31973  mapdh8i  31977  mapdh8j  31978  mapdh9a  31980  mapdh9aOLDN  31981  hdmap1l6d  32004  hdmap1l6e  32005  hdmap1l6f  32006  hdmap1l6j  32010  hdmapval2  32025  hdmapeveclem  32027  hdmapval3lemN  32030  hdmap11lem1  32034  hgmapfval  32079  hlhils0  32138  hlhils1N  32139  hlhillvec  32144  hlhildrng  32145  hlhil0  32148  hlhillsm  32149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator