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

Theorem eqidd 2359
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 2358 . 2  |-  A  =  A
21a1i 10 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642
This theorem is referenced by:  nfabd2  2512  cbvraldva  2846  cbvrexdva  2847  opeq1  3875  opeq2  3876  mpteq1  4179  nfcvb  4284  tfisi  4728  iotanul  5313  feq23d  5466  fvmptdv2  5693  fmptco  5771  fprg  5785  fliftfun  5895  fliftval  5899  cbvmpt2  6009  eqfnov2  6035  ovmpt2d  6059  ovmpt2dv2  6065  ofval  6171  ofrval  6172  offn  6173  fnfvof  6174  off  6177  ofres  6178  ofco  6181  caofref  6187  caofid0l  6189  caofid0r  6190  caofid1  6191  caofid2  6192  caofrss  6194  caoftrn  6196  suppssof1  6203  riotabidv  6390  nfriotad  6397  iserd  6770  ixpsnf1o  6941  mapxpen  7112  dffi3  7271  oieq1  7314  oieq2  7315  cantnfp1  7470  cantnflem1d  7477  cantnflem1  7478  iunfictbso  7828  axcclem  8170  ttukeylem3  8225  ttukey2g  8230  fpwwe2lem9  8347  wunex2  8447  wuncval2  8456  ofsubeq0  9830  ofnegsub  9831  ofsubge0  9832  seqeq2  11139  seqeq3  11140  seqid  11180  seqid2  11181  seqz  11183  seqof  11192  bcval  11407  swrdval  11540  wrdind  11567  revco  11579  ccatco  11580  rlim2  12060  climcl  12063  rlimcl  12067  clim2  12068  lo1o12  12097  rlimclim1  12109  rlimclim  12110  climrlim2  12111  climuni  12116  rlimres  12122  climeq  12131  2clim  12136  climshftlem  12138  climabs0  12149  rlimcn1b  12153  climcn1  12155  climcn2  12156  o1of2  12176  o1rlimmul  12182  o1add2  12187  o1mul2  12188  o1sub2  12189  o1dif  12193  climsqz  12204  climsqz2  12205  rlimdiv  12209  isercoll  12231  climsup  12233  climcau  12234  caurcvgr  12237  caucvgb  12243  serf0  12244  iseralt  12248  cbvsum  12259  summolem2a  12279  zsum  12282  fsum  12284  sumz  12286  sumss  12288  fsumss  12289  sumss2  12290  fsumcvg2  12291  fsumser  12294  isumclim3  12313  isummulc2  12316  fsum2dlem  12324  fsumconst  12343  fsumabs  12350  fsumparts  12355  fsumrlim  12360  fsumo1  12361  seqabs  12363  cvgcmpce  12367  fsumiun  12370  ackbijnn  12377  isumshft  12389  isumless  12395  isumltss  12398  climcndslem1  12399  climcndslem2  12400  climcnds  12401  mertenslem1  12431  mertenslem2  12432  eftlcl  12478  reeftlcl  12479  eftlub  12480  efsep  12481  effsumlt  12482  eirrlem  12573  rpnnen2lem1  12584  rpnnen2lem6  12589  rpnnen2lem7  12590  rpnnen2lem8  12591  rpnnen2lem9  12592  rpnnen2  12595  rpnnen  12596  bitsp1  12713  sadadd2lem  12741  sadadd2  12742  sadasslem  12752  smupvallem  12765  smumul  12775  alginv  12836  algfx  12841  qnumdencoprm  12907  qeqnumdivden  12908  pcmpt  13031  pcmptdvds  13033  prmreclem2  13055  prmreclem4  13057  prmreclem5  13058  prmreclem6  13059  prmrec  13060  vdwlem1  13119  vdwlem12  13130  vdwlem13  13131  ramub1lem2  13165  ramcl  13167  prdssca  13449  prdsbas  13450  prdsplusg  13451  prdsmulr  13452  prdsvsca  13453  prdsle  13454  prdsds  13456  prdstset  13458  prdshom  13459  prdsco  13460  prdsvscafval  13472  prdsdsval2  13476  prdsdsval3  13477  pwsle  13484  pwsleval  13485  pwsvscaval  13487  imasbas  13508  imasds  13509  imasplusg  13513  imasmulr  13514  imassca  13515  imasvsca  13516  imastset  13517  imasle  13518  imasvscafn  13532  imasvscaval  13533  divsin  13539  xpsvsca  13574  mrcfval  13603  iscat  13667  iscatd  13668  catidex  13669  cidval  13672  catidd  13675  iscatd2  13676  catlid  13678  catrid  13679  0catg  13682  homfeq  13690  homfeqd  13691  comfffval2  13697  comffval2  13698  comfeq  13702  comfeqd  13703  oppccatid  13715  2oppccomf  13721  ismon  13729  moni  13732  ssc2  13792  ssctr  13795  ssceq  13796  subcssc  13807  subccat  13815  subsubc  13820  isfunc  13831  funcres  13863  funcres2  13865  funcres2c  13868  idffth  13900  cofull  13901  cofth  13902  ressffth  13905  isnat  13914  fuccofval  13926  fucco  13929  fuccatid  13936  fucpropd  13944  elhomai  13958  coafval  13989  setcval  14002  setcbas  14003  setchomfval  14004  setccofval  14007  setcco  14008  setccatid  14009  setcepi  14013  funcsetcres2  14018  catcval  14021  catcbas  14022  catchomfval  14023  catccofval  14025  catcco  14026  catccatid  14027  catciso  14032  catcfuccl  14034  xpcbas  14045  xpchomfval  14046  xpccofval  14049  xpccatid  14055  1stfcl  14064  2ndfcl  14065  prfval  14066  catcxpccl  14074  xpcpropd  14075  evlfval  14084  curfval  14090  curf1  14092  curf12  14094  curf2  14096  curf2val  14097  curfpropd  14100  hofval  14119  hof2fval  14122  hofcllem  14125  oppchofcl  14127  oppcyon  14136  oyoncl  14137  yonedalem4a  14142  yonedalem4b  14143  yonedalem4c  14144  yonedalem3b  14146  yonedainv  14148  oduposb  14333  ipopos  14356  isdlat  14389  ismnd  14462  ismndd  14489  mndprop  14493  prdsmndd  14498  imasmnd2  14502  gsumpropd  14546  gsumval1  14549  gsumval2a  14552  frmdbas  14567  frmdmnd  14574  grpprop  14594  grpsubfval  14617  grpsubpropd  14659  mulgfval  14661  mulgpropd  14693  prdsgrpd  14697  imasgrp2  14703  imasgrp  14704  imasgrpf1  14705  subgsub  14726  eqgfval  14758  divsgrp  14765  symgval  14864  symggrp  14873  oppgmnd  14920  oppgmndb  14921  oppggrp  14923  oppggrpb  14924  odfval  14941  oppglsm  15046  lsmelvalmi  15056  efgi0  15122  efgi1  15123  efgtf  15124  efgval2  15126  efginvrel2  15129  frgp0  15162  frgpup3lem  15179  ablprop  15193  subcmn  15226  gex2abl  15236  prdscmnd  15246  divsabl  15250  cyggenod2  15265  cygabl  15270  gsumzf1o  15289  gsumzaddlem  15296  gsumzsplit  15299  gsumconst  15302  gsummhm2  15305  gsumunsn  15314  gsumpt  15315  gsum2d  15316  gsumcom2  15319  dprdval  15331  dprdssv  15344  dprdfeq0  15350  dprdsubg  15352  dprdspan  15355  dprdz  15358  subgdmdprd  15362  subgdprd  15363  dmdprdsplitlem  15365  dprd2d2  15372  isrng  15438  rngabl  15463  rngprop  15467  isrngd  15468  prdsrngd  15488  prdscrngd  15489  prds1  15490  imasrng  15495  opprrng  15506  opprrngb  15507  dvrfval  15559  pwsco1rhm  15603  pwsco2rhm  15604  drngprop  15616  isdrngd  15630  isdrngrd  15631  pwsdiagrhm  15671  abvtrivd  15698  islmodd  15726  lmodabl  15765  lss1  15789  lsssn0  15798  islss3  15809  lss1d  15813  lssintcl  15814  prdslmodd  15819  idlmhm  15891  invlmhm  15892  lmhmvsca  15895  lbsextlem2  16005  sralmod  16032  sralmod0  16033  rlm0  16043  rlmvneg  16052  crngridl  16083  divscrng  16085  isassa  16149  isassad  16156  issubassa  16157  sraassa  16158  asclfval  16167  ressascl  16176  psrval  16203  psrbaglesupp  16207  psrbagcon  16210  psrbaglefi  16211  psrbagconf1o  16213  gsumbagdiaglem  16214  psrass1lem  16216  psrbas  16217  psrplusg  16219  psrmulr  16222  psrsca  16227  psrvscafval  16228  psrvscaval  16230  psrgrp  16236  psrlmod  16239  psrlidm  16241  psrdi  16244  psrdir  16245  psrcom  16246  psrrng  16248  psrassa  16251  mplsubglem  16272  mpllsslem  16273  mplvscaval  16285  mplcoe1  16302  mplcoe3  16303  mplcoe2  16304  opsrcrng  16322  opsrassa  16323  mplmon2  16327  evlslem2  16342  ply1lss  16368  ply1subrg  16369  opsr0  16388  opsr1  16389  subrgply1  16404  psrplusgpropd  16406  psropprmul  16409  opsrrng  16416  opsrlmod  16417  ply1mpl0  16426  ply1mpl1  16427  coe1z  16433  coe1mul2  16439  coe1tm  16442  coe1tmmul2fv  16447  coe1pwmulfv  16449  coe1sclmulfv  16452  ply1coe  16461  absabv  16529  zrhpropd  16569  znzrh  16596  znbas  16597  zncrng  16598  znzrhfo  16601  znf1o  16605  cyggic  16626  frgpcyg  16627  isphld  16658  phlpropd  16659  pjfval  16706  epttop  16846  ordtbas2  17021  ordtopn1  17024  ordtopn2  17025  lmss  17126  2ndci  17274  2ndcsep  17285  dis2ndc  17286  1stcelcls  17287  ptbasid  17370  xkoopn  17384  prdstopn  17422  ptrescn  17433  txlm  17442  lmcn2  17443  tx1stc  17444  xkopt  17449  cnmpt2c  17464  cnmptk1  17475  cnmpt1k  17476  cnmptkk  17477  qtopeu  17507  txswaphmeolem  17595  xpstopnlem1  17600  ptcmpfi  17604  xkohmeo  17606  rnelfmlem  17743  rnelfm  17744  hauspwpwf1  17778  lmflf  17796  flfcnp2  17798  fclsval  17799  alexsubb  17836  tmdgsum  17874  tgpconcomp  17891  divstgphaus  17901  tsmsfbas  17906  tsmspropd  17910  tsms0  17920  tsmsmhm  17924  tgptsmscls  17928  tsmssplit  17930  tsmsxplem1  17931  tsmsxplem2  17932  imasdsf1olem  18033  blfval  18043  stdbdmetval  18156  stdbdxmet  18157  met2ndci  18164  prdsxmslem2  18171  nmfval  18207  nmpropd  18212  nmpropd2  18213  subgnm  18245  tng0  18255  tngnm  18263  tngnrg  18281  sranlm  18291  qdensere  18375  fsumcn  18471  cncfmpt1f  18514  negfcncf  18520  oprpiece1res2  18548  htpyid  18573  phtpyid  18585  pcofval  18606  pcopt2  18619  om1bas  18627  om1plusg  18630  om1tset  18631  pi1bas  18634  pi1bas2  18637  pi1eluni  18638  pi1bas3  18639  pi1cpbl  18640  pi1addf  18643  pi1addval  18644  pi1grplem  18645  pi1xfr  18651  pi1xfrcnvlem  18652  pi1coghm  18657  cphassr  18745  tchphl  18756  ipcau2  18762  lmnn  18787  iscau  18800  cmetcaulem  18812  iscmet3lem1  18815  causs  18822  lmclim  18826  srabn  18875  ovollb2lem  18945  ovolfiniun  18958  ovolicc2lem3  18976  ovolicc2lem4  18977  ovolicc2lem5  18978  shftmbl  18994  volfiniun  19002  ioombl1lem4  19016  uniioombllem2  19036  uniioombllem3  19038  uniioombllem6  19041  vitalilem4  19064  ismbfcn2  19092  mbfmulc2lem  19100  mbfmulc2re  19101  mbfneg  19103  mbfposb  19106  mbfaddlem  19113  mbfadd  19114  mbfsub  19115  mbfmulc2  19116  0plef  19125  0pledm  19126  itg1ge0  19139  i1faddlem  19146  i1fmullem  19147  i1fmulclem  19155  itg1mulc  19157  i1fres  19158  i1fposd  19160  itg1lea  19165  itg1le  19166  itg1climres  19167  mbfi1fseqlem2  19169  mbfi1fseq  19174  mbfi1flimlem  19175  mbfi1flim  19176  mbfmullem2  19177  mbfmul  19179  xrge0f  19184  itg2ge0  19188  itg2const  19193  itg2const2  19194  itg2uba  19196  itg2lea  19197  itg2splitlem  19201  itg2split  19202  itg2monolem1  19203  itg2mono  19206  itg2i1fseqle  19207  itg2i1fseq  19208  itg2addlem  19211  itg2gt0  19213  itg2cnlem1  19214  itg2cnlem2  19215  itg2cn  19216  isibl  19218  isibl2  19219  iblitg  19221  dfitg  19222  cbvitg  19228  itgeq2  19230  itgcl  19236  itgvallem  19237  ibl0  19239  iblcnlem1  19240  itgcnlem  19242  iblneg  19255  itgneg  19256  iblss  19257  iblss2  19258  i1fibl  19260  itgitg1  19261  itgle  19262  itgeqa  19266  itgss3  19267  iblconst  19270  ibladdlem  19272  ibladd  19273  itgaddlem1  19275  itgfsum  19279  iblabslem  19280  iblabs  19281  iblabsr  19282  iblmulc2  19283  itgmulc2lem1  19284  itgsplit  19288  bddmulibl  19291  bddibl  19292  itgcn  19295  limccnp  19339  limccnp2  19340  limcco  19341  dvidlem  19363  dvcnp2  19367  dvaddbr  19385  dvmulbr  19386  dvaddf  19389  dvcmulf  19392  dvcobr  19393  dvcjbr  19396  dvexp  19400  dvmptadd  19407  dvmptmul  19408  dvmptcj  19415  dvmptco  19419  dvmptfsum  19420  dvcnvlem  19421  dvef  19425  rolle  19435  mvth  19437  dvlip  19438  dvlipcn  19439  lhop1lem  19458  itgsubstlem  19493  evlslem1  19497  mpfrcl  19500  evlsval  19501  evl1rhm  19510  evl1sca  19511  evl1expd  19519  deg1suble  19591  ply1divalg2  19622  uc1pmon1p  19635  q1pval  19637  r1pval  19640  elply2  19676  elplyr  19681  plypf1  19692  plyaddlem1  19693  coeeulem  19704  plyco  19721  coeaddlem  19728  coemulc  19734  dgradd2  19747  dgrsub  19751  dgrcolem1  19752  dgrcolem2  19753  dgrco  19754  ofmulrt  19760  plydivlem3  19773  plydivlem4  19774  plyrem  19783  iaa  19803  aareccl  19804  aannenlem2  19807  aaliou3lem3  19822  aaliou3lem7  19827  taylfval  19836  taylply2  19845  dvntaylp  19848  taylthlem2  19851  ulmclm  19864  ulmres  19865  ulmshftlem  19866  ulm0  19868  ulmcau  19872  ulmss  19874  ulmbdd  19875  ulmcn  19876  mtest  19881  mtestbdd  19882  iblulm  19884  itgulm  19885  pserulm  19899  pserdvlem2  19905  abelthlem5  19912  abelthlem6  19913  abelthlem8  19916  abelthlem9  19917  sincn  19921  coscn  19922  efcvx  19926  logfac  20056  logcn  20099  chordthmlem  20234  chordthmlem5  20238  mcubic  20248  leibpi  20343  efrlim  20369  amgmlem  20389  basellem7  20430  basellem9  20432  vmaval  20457  prmorcht  20522  musum  20537  chtublem  20556  pclogsum  20560  logexprlim  20570  dchrbas  20580  dchrelbasd  20584  dchr1cl  20596  dchrabl  20599  dchrfi  20600  dchrptlem2  20610  dchrhash  20616  bposlem5  20633  bposlem6  20634  lgsfval  20646  lgsdir2lem5  20672  lgsdir  20675  lgsdilem2  20676  lgsdi  20677  lgsne0  20678  lgseisenlem2  20695  lgseisenlem3  20696  lgseisenlem4  20697  lgsquad2lem2  20704  2sqlem8  20717  2sqlem11  20720  chtppilimlem2  20729  chebbnd2  20732  chpchtlim  20734  chpo1ub  20735  vmadivsum  20737  rplogsumlem2  20740  rpvmasumlem  20742  dchrisum0re  20768  dchrisum0  20775  mudivsum  20785  selberglem1  20800  selberglem2  20801  selberg2lem  20805  selberg2  20806  pntrsumo1  20820  selbergr  20823  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  abvcxp  20870  grpodivfval  21015  gxfval  21030  isrngo  21151  dipfval  21383  ipval2  21388  lnoval  21438  ajfval  21495  minvecolem3  21563  h2hcau  21667  h2hlm  21668  opsqrlem3  22830  opsqrlem4  22831  disjdifprg  23213  iundisjf  23224  ofrn2  23254  off2  23255  fmptcof2  23277  cofmpt  23279  ressnm  23389  abvpropd2  23390  gsumpropd2lem  23412  gsumconstf  23414  tpr2rico  23466  fmcncfil  23473  lmdvglim  23495  ustuqtop4  23548  metustexhalf  23600  cfilucfil  23603  restmetu  23615  nmmulg  23627  qqhval  23631  qqhval2  23639  indf1ofs  23689  esumeq1  23697  esumeq1d  23698  esumeq2d  23700  esumc  23712  esumsplit  23713  gsumesum  23717  esumlub  23718  esumcst  23721  esumsn  23722  esumpinfval  23729  esumcocn  23736  esummulc1  23737  hasheuni  23741  esumcvg  23742  ofcval  23748  ofcfn  23749  ofcfeqd2  23750  ofcf  23752  ofcfval4  23754  sigaval  23759  issgon  23772  sxval  23810  measvunilem0  23831  measvuni  23832  meascnbl  23837  volmeas  23851  sxbrsiga  23904  itgeq12dv  23905  totprobd  23933  probfinmeasb  23936  probmeasb  23937  rrvadd  23959  orvcval4  23967  dstfrvclim1  23984  ballotlemsval  24015  ballotlemieq  24023  quartfull  24045  lgamgulmlem2  24063  lgamcvglem  24073  lgamcvg2  24088  sconpi1  24174  cvmliftphtlem  24252  cvmlift3lem2  24255  eupath2lem2  24306  sinccvg  24410  circum  24411  relexp0  24429  relexpsucr  24430  rtrclreclem.subset  24446  rtrclreclem.min  24448  dfrtrcl2  24449  cbvprod  24542  prodmolem2a  24561  zprod  24564  fprod  24568  fprodntriv  24569  prod1  24571  prodss  24574  fprodss  24575  fprodconst  24603  iprodclim3  24607  br8  24671  br4  24673  trpred0  24797  elno2  24866  brsegle  25290  hilbert1.1  25336  volsupnfl  25491  itg2addnclem  25492  itg2addnc  25494  itg2gt0cn  25495  ibladdnclem  25496  itgaddnclem1  25498  itgaddnclem2  25499  itgaddnc  25500  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nclem1  25506  itgmulc2nclem2  25507  itgmulc2nc  25508  bddiblnc  25510  ftc1cnnclem  25513  areacirc  25523  trer  25551  tailfval  25645  unirep  25673  upixp  25727  sdc  25778  lmclim2  25798  geomcau  25799  caures  25800  caushft  25801  prdsbnd2  25842  heibor1lem  25856  bfplem2  25870  rrncmslem  25879  eldiophb  26159  eldioph  26160  eldioph3  26168  rabren3dioph  26221  pellqrexplicit  26285  rmxycomplete  26325  rmxynorm  26326  acongrep  26390  jm2.26a  26416  jm2.26  26418  fnwe2lem2  26471  fnwe2lem3  26472  aomclem5  26478  aomclem8  26482  dsmmval  26523  dsmmsubg  26532  imasgim  26587  isnumbasgrplem1  26589  islindf  26605  islindf4  26631  hbtlem5  26655  dgrsub2  26662  rgspnid  26700  rngunsnply  26701  pmtrval  26717  symgsssg  26731  symgfisg  26732  psgnunilem4  26743  psgnvalii  26755  mamufval  26766  mamuval  26767  mamudi  26784  mamudir  26785  mat0  26795  matinvg  26796  matlmod  26802  matrng  26803  matassa  26804  mdetfval  26810  mendval  26814  mendrng  26823  mendlmod  26824  mendassa  26825  caofcan  26863  ofsubid  26864  ofmul12  26865  ofdivrec  26866  ofdivcan4  26867  ofdivdiv2  26868  expgrowth  26875  fmuldfeqlem1  27035  clim1fr1  27050  climrec  27052  climexp  27054  climinf  27055  climsuse  27057  climneg  27059  stoweidlem2  27074  stoweidlem17  27089  stoweidlem21  27093  stoweidlem31  27103  stoweidlem32  27104  stoweidlem34  27106  stoweidlem44  27116  stoweidlem46  27118  stoweidlem55  27127  wallispi  27142  wallispi2lem1  27143  wallispi2lem2  27144  wallispi2  27145  stirlinglem1  27146  stirlinglem3  27148  stirlinglem5  27150  stirlinglem6  27151  stirlinglem14  27159  afveq12d  27321  afveq1  27322  afveq2  27323  afvco2  27364  rspceaov  27385  ffnaov  27387  faovcl  27388  ftpg  27414  elrnrexdm  27424  fzo0to3tp  27455  s2f1o  27494  s4f1o  27496  usgra0v  27538  usgra1v  27555  usgraexvlem  27560  usgrares1  27570  nbgranself  27592  wlkonwlk  27670  0pthon1  27705  constr3trllem2  27758  frgra3vlem1  27816  3vfriswmgralem  27820  frgrancvvdeqlem2  27847  lflset  29301  islfld  29304  lfladdcl  29313  lflvscl  29319  lkrsc  29339  eqlkr2  29342  lshpkrlem1  29352  ldualset  29367  ldualvaddval  29373  ldualvsval  29380  ldualgrplem  29387  lduallmodlem  29394  cmtfvalN  29452  isoml  29480  iscvlat  29565  llni2  29753  lplni2  29778  lvoli3  29818  lvoli2  29822  paddfval  30038  lhpset  30236  ltrnfset  30358  trlfset  30401  cdleme21k  30579  cdlemeiota  30826  tgrpfset  30985  tgrpset  30986  tgrpabl  30992  tendo0cbv  31027  tendo02  31028  erngfset  31040  erngset  31041  erngfset-rN  31048  erngset-rN  31049  cdlemk40  31158  cdlemkid5  31176  cdlemkid  31177  dvafset  31245  dvaset  31246  diaffval  31272  dialss  31288  diaf11N  31291  dvhfset  31322  dvhset  31323  docaffvalN  31363  dibfval  31383  dibf11N  31403  diblss  31412  diclss  31435  dihord2cN  31463  dihord11b  31464  dihffval  31472  dihord6apre  31498  dihglblem2aN  31535  dihglblem2N  31536  dihjatcclem4  31663  lclkrs  31781  mapdh6dN  31981  mapdh6eN  31982  mapdh6fN  31983  mapdh6jN  31987  hvmapffval  32000  hvmapfval  32001  mapdh8a  32017  mapdh8ad  32021  mapdh8d0N  32024  mapdh8d  32025  mapdh8i  32029  mapdh8j  32030  mapdh9a  32032  mapdh9aOLDN  32033  hdmap1l6d  32056  hdmap1l6e  32057  hdmap1l6f  32058  hdmap1l6j  32062  hdmapval2  32077  hdmapeveclem  32079  hdmapval3lemN  32082  hdmap11lem1  32086  hgmapfval  32131  hlhils0  32190  hlhils1N  32191  hlhillvec  32196  hlhildrng  32197  hlhil0  32200  hlhillsm  32201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-cleq 2351
  Copyright terms: Public domain W3C validator