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

Theorem eqidd 2297
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 2296 . 2  |-  A  =  A
21a1i 10 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  nfabd2  2450  cbvraldva  2783  cbvrexdva  2784  opeq1  3812  opeq2  3813  mpteq1  4116  nfcvb  4221  tfisi  4665  iotanul  5250  feq23d  5402  fvmptdv2  5629  fmptco  5707  fliftfun  5827  fliftval  5831  cbvmpt2  5941  eqfnov2  5967  ovmpt2d  5991  ovmpt2dv2  5997  ofval  6103  ofrval  6104  offn  6105  fnfvof  6106  off  6109  ofres  6110  ofco  6113  caofref  6119  caofid0l  6121  caofid0r  6122  caofid1  6123  caofid2  6124  caofrss  6126  caoftrn  6128  suppssof1  6135  riotabidv  6322  nfriotad  6329  iserd  6702  ixpsnf1o  6872  mapxpen  7043  dffi3  7200  oieq1  7243  oieq2  7244  cantnfp1  7399  cantnflem1d  7406  cantnflem1  7407  iunfictbso  7757  axcclem  8099  ttukeylem3  8154  ttukey2g  8159  fpwwe2lem9  8276  wunex2  8376  wuncval2  8385  ofsubeq0  9759  ofnegsub  9760  ofsubge0  9761  seqeq2  11066  seqeq3  11067  seqid  11107  seqid2  11108  seqz  11110  seqof  11119  bcval  11333  swrdval  11466  wrdind  11493  revco  11505  ccatco  11506  rlim2  11986  climcl  11989  rlimcl  11993  clim2  11994  lo1o12  12023  rlimclim1  12035  rlimclim  12036  climrlim2  12037  climuni  12042  rlimres  12048  climeq  12057  2clim  12062  climshftlem  12064  climabs0  12075  rlimcn1b  12079  climcn1  12081  climcn2  12082  o1of2  12102  o1rlimmul  12108  o1add2  12113  o1mul2  12114  o1sub2  12115  o1dif  12119  climsqz  12130  climsqz2  12131  rlimdiv  12135  isercoll  12157  climsup  12159  climcau  12160  caurcvgr  12162  caucvgb  12168  serf0  12169  iseralt  12173  cbvsum  12184  summolem2a  12204  zsum  12207  fsum  12209  sumz  12211  sumss  12213  fsumss  12214  sumss2  12215  fsumcvg2  12216  fsumser  12219  isumclim3  12238  isummulc2  12241  fsum2dlem  12249  fsumconst  12268  fsumabs  12275  fsumparts  12280  fsumrlim  12285  fsumo1  12286  seqabs  12288  cvgcmpce  12292  fsumiun  12295  ackbijnn  12302  isumshft  12314  isumless  12320  isumltss  12323  climcndslem1  12324  climcndslem2  12325  climcnds  12326  mertenslem1  12356  mertenslem2  12357  eftlcl  12403  reeftlcl  12404  eftlub  12405  efsep  12406  effsumlt  12407  eirrlem  12498  rpnnen2lem1  12509  rpnnen2lem6  12514  rpnnen2lem7  12515  rpnnen2lem8  12516  rpnnen2lem9  12517  rpnnen2  12520  rpnnen  12521  bitsp1  12638  sadadd2lem  12666  sadadd2  12667  sadasslem  12677  smupvallem  12690  smumul  12700  alginv  12761  algfx  12766  qnumdencoprm  12832  qeqnumdivden  12833  pcmpt  12956  pcmptdvds  12958  prmreclem2  12980  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  prmrec  12985  vdwlem1  13044  vdwlem12  13055  vdwlem13  13056  ramub1lem2  13090  ramcl  13092  prdssca  13372  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsle  13377  prdsds  13379  prdstset  13381  prdshom  13382  prdsco  13383  prdsvscafval  13395  prdsdsval2  13399  prdsdsval3  13400  pwsle  13407  pwsleval  13408  pwsvscaval  13410  imasbas  13431  imasds  13432  imasplusg  13436  imasmulr  13437  imassca  13438  imasvsca  13439  imastset  13440  imasle  13441  imasvscafn  13455  imasvscaval  13456  divsin  13462  xpsvsca  13497  mrcfval  13526  iscat  13590  iscatd  13591  catidex  13592  cidval  13595  catidd  13598  iscatd2  13599  catlid  13601  catrid  13602  0catg  13605  homfeq  13613  homfeqd  13614  comfffval2  13620  comffval2  13621  comfeq  13625  comfeqd  13626  oppccatid  13638  2oppccomf  13644  ismon  13652  moni  13655  ssc2  13715  ssctr  13718  ssceq  13719  subcssc  13730  subccat  13738  subsubc  13743  isfunc  13754  funcres  13786  funcres2  13788  funcres2c  13791  idffth  13823  cofull  13824  cofth  13825  ressffth  13828  isnat  13837  fuccofval  13849  fucco  13852  fuccatid  13859  fucpropd  13867  elhomai  13881  coafval  13912  setcval  13925  setcbas  13926  setchomfval  13927  setccofval  13930  setcco  13931  setccatid  13932  setcepi  13936  funcsetcres2  13941  catcval  13944  catcbas  13945  catchomfval  13946  catccofval  13948  catcco  13949  catccatid  13950  catciso  13955  catcfuccl  13957  xpcbas  13968  xpchomfval  13969  xpccofval  13972  xpccatid  13978  1stfcl  13987  2ndfcl  13988  prfval  13989  catcxpccl  13997  xpcpropd  13998  evlfval  14007  curfval  14013  curf1  14015  curf12  14017  curf2  14019  curf2val  14020  curfpropd  14023  hofval  14042  hof2fval  14045  hofcllem  14048  oppchofcl  14050  oppcyon  14059  oyoncl  14060  yonedalem4a  14065  yonedalem4b  14066  yonedalem4c  14067  yonedalem3b  14069  yonedainv  14071  oduposb  14256  ipopos  14279  isdlat  14312  ismnd  14385  ismndd  14412  mndprop  14416  prdsmndd  14421  imasmnd2  14425  gsumpropd  14469  gsumval1  14472  gsumval2a  14475  frmdbas  14490  frmdmnd  14497  grpprop  14517  grpsubfval  14540  grpsubpropd  14582  mulgfval  14584  mulgpropd  14616  prdsgrpd  14620  imasgrp2  14626  imasgrp  14627  imasgrpf1  14628  subgsub  14649  eqgfval  14681  divsgrp  14688  symgval  14787  symggrp  14796  oppgmnd  14843  oppgmndb  14844  oppggrp  14846  oppggrpb  14847  odfval  14864  oppglsm  14969  lsmelvalmi  14979  efgi0  15045  efgi1  15046  efgtf  15047  efgval2  15049  efginvrel2  15052  frgp0  15085  frgpup3lem  15102  ablprop  15116  subcmn  15149  gex2abl  15159  prdscmnd  15169  divsabl  15173  cyggenod2  15188  cygabl  15193  gsumzf1o  15212  gsumzaddlem  15219  gsumzsplit  15222  gsumconst  15225  gsummhm2  15228  gsumunsn  15237  gsumpt  15238  gsum2d  15239  gsumcom2  15242  dprdval  15254  dprdssv  15267  dprdfeq0  15273  dprdsubg  15275  dprdspan  15278  dprdz  15281  subgdmdprd  15285  subgdprd  15286  dmdprdsplitlem  15288  dprd2d2  15295  isrng  15361  rngabl  15386  rngprop  15390  isrngd  15391  prdsrngd  15411  prdscrngd  15412  prds1  15413  imasrng  15418  opprrng  15429  opprrngb  15430  dvrfval  15482  pwsco1rhm  15526  pwsco2rhm  15527  drngprop  15539  isdrngd  15553  isdrngrd  15554  pwsdiagrhm  15594  abvtrivd  15621  islmodd  15649  lmodabl  15688  lss1  15712  lsssn0  15721  islss3  15732  lss1d  15736  lssintcl  15737  prdslmodd  15742  idlmhm  15814  invlmhm  15815  lmhmvsca  15818  lbsextlem2  15928  sralmod  15955  sralmod0  15956  rlm0  15966  rlmvneg  15975  crngridl  16006  divscrng  16008  isassa  16072  isassad  16079  issubassa  16080  sraassa  16081  asclfval  16090  ressascl  16099  psrval  16126  psrbaglesupp  16130  psrbagcon  16133  psrbaglefi  16134  psrbagconf1o  16136  gsumbagdiaglem  16137  psrass1lem  16139  psrbas  16140  psrplusg  16142  psrmulr  16145  psrsca  16150  psrvscafval  16151  psrvscaval  16153  psrgrp  16159  psrlmod  16162  psrlidm  16164  psrdi  16167  psrdir  16168  psrcom  16169  psrrng  16171  psrassa  16174  mplsubglem  16195  mpllsslem  16196  mplvscaval  16208  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  opsrcrng  16245  opsrassa  16246  mplmon2  16250  evlslem2  16265  ply1lss  16291  ply1subrg  16292  opsr0  16311  opsr1  16312  subrgply1  16327  psrplusgpropd  16329  psropprmul  16332  opsrrng  16339  opsrlmod  16340  ply1mpl0  16349  ply1mpl1  16350  coe1z  16356  coe1mul2  16362  coe1tm  16365  coe1tmmul2fv  16370  coe1pwmulfv  16372  coe1sclmulfv  16375  ply1coe  16384  absabv  16445  zrhpropd  16485  znzrh  16512  znbas  16513  zncrng  16514  znzrhfo  16517  znf1o  16521  cyggic  16542  frgpcyg  16543  isphld  16574  phlpropd  16575  pjfval  16622  epttop  16762  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  lmss  17042  2ndci  17190  2ndcsep  17201  dis2ndc  17202  1stcelcls  17203  ptbasid  17286  xkoopn  17300  prdstopn  17338  ptrescn  17349  txlm  17358  lmcn2  17359  tx1stc  17360  xkopt  17365  cnmpt2c  17380  cnmptk1  17391  cnmpt1k  17392  cnmptkk  17393  qtopeu  17423  txswaphmeolem  17511  xpstopnlem1  17516  ptcmpfi  17520  xkohmeo  17522  rnelfmlem  17663  rnelfm  17664  hauspwpwf1  17698  lmflf  17716  flfcnp2  17718  fclsval  17719  alexsubb  17756  tmdgsum  17794  tgpconcomp  17811  divstgphaus  17821  tsmsfbas  17826  tsmspropd  17830  tsms0  17840  tsmsmhm  17844  tgptsmscls  17848  tsmssplit  17850  tsmsxplem1  17851  tsmsxplem2  17852  imasdsf1olem  17953  blfval  17963  stdbdmetval  18076  stdbdxmet  18077  met2ndci  18084  prdsxmslem2  18091  nmfval  18127  nmpropd  18132  nmpropd2  18133  subgnm  18165  tng0  18175  tngnm  18183  tngnrg  18201  sranlm  18211  qdensere  18295  fsumcn  18390  cncfmpt1f  18433  negfcncf  18438  oprpiece1res2  18466  htpyid  18491  phtpyid  18503  pcofval  18524  pcopt2  18537  om1bas  18545  om1plusg  18548  om1tset  18549  pi1bas  18552  pi1bas2  18555  pi1eluni  18556  pi1bas3  18557  pi1cpbl  18558  pi1addf  18561  pi1addval  18562  pi1grplem  18563  pi1xfr  18569  pi1xfrcnvlem  18570  pi1coghm  18575  cphassr  18663  tchphl  18674  ipcau2  18680  lmnn  18705  iscau  18718  cmetcaulem  18730  iscmet3lem1  18733  causs  18740  lmclim  18744  srabn  18793  ovollb2lem  18863  ovolfiniun  18876  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  shftmbl  18912  volfiniun  18920  ioombl1lem4  18934  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  vitalilem4  18982  ismbfcn2  19010  mbfmulc2lem  19018  mbfmulc2re  19019  mbfneg  19021  mbfposb  19024  mbfaddlem  19031  mbfadd  19032  mbfsub  19033  mbfmulc2  19034  0plef  19043  0pledm  19044  itg1ge0  19057  i1faddlem  19064  i1fmullem  19065  i1fmulclem  19073  itg1mulc  19075  i1fres  19076  i1fposd  19078  itg1lea  19083  itg1le  19084  itg1climres  19085  mbfi1fseqlem2  19087  mbfi1fseq  19092  mbfi1flimlem  19093  mbfi1flim  19094  mbfmullem2  19095  mbfmul  19097  xrge0f  19102  itg2ge0  19106  itg2const  19111  itg2const2  19112  itg2uba  19114  itg2lea  19115  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  isibl  19136  isibl2  19137  iblitg  19139  dfitg  19140  cbvitg  19146  itgeq2  19148  itgcl  19154  itgvallem  19155  ibl0  19157  iblcnlem1  19158  itgcnlem  19160  iblneg  19173  itgneg  19174  iblss  19175  iblss2  19176  i1fibl  19178  itgitg1  19179  itgle  19180  itgeqa  19184  itgss3  19185  iblconst  19188  ibladdlem  19190  ibladd  19191  itgaddlem1  19193  itgfsum  19197  iblabslem  19198  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2lem1  19202  itgsplit  19206  bddmulibl  19209  bddibl  19210  itgcn  19213  limccnp  19257  limccnp2  19258  limcco  19259  dvidlem  19281  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvaddf  19307  dvcmulf  19310  dvcobr  19311  dvcjbr  19314  dvexp  19318  dvmptadd  19325  dvmptmul  19326  dvmptcj  19333  dvmptco  19337  dvmptfsum  19338  dvcnvlem  19339  dvef  19343  rolle  19353  mvth  19355  dvlip  19356  dvlipcn  19357  lhop1lem  19376  itgsubstlem  19411  evlslem1  19415  mpfrcl  19418  evlsval  19419  evl1rhm  19428  evl1sca  19429  evl1expd  19437  deg1suble  19509  ply1divalg2  19540  uc1pmon1p  19553  q1pval  19555  r1pval  19558  elply2  19594  elplyr  19599  plypf1  19610  plyaddlem1  19611  coeeulem  19622  plyco  19639  coeaddlem  19646  coemulc  19652  dgradd2  19665  dgrsub  19669  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  ofmulrt  19678  plydivlem3  19691  plydivlem4  19692  plyrem  19701  iaa  19721  aareccl  19722  aannenlem2  19725  aaliou3lem3  19740  aaliou3lem7  19745  taylfval  19754  taylply2  19763  dvntaylp  19766  taylthlem2  19769  ulmclm  19782  ulmres  19783  ulmshftlem  19784  ulm0  19786  ulmcau  19788  ulmss  19790  ulmbdd  19791  ulmcn  19792  mtest  19797  iblulm  19799  itgulm  19800  pserulm  19814  pserdvlem2  19820  abelthlem5  19827  abelthlem6  19828  abelthlem8  19831  abelthlem9  19832  sincn  19836  coscn  19837  efcvx  19841  logfac  19970  logcn  20010  chordthmlem  20145  chordthmlem5  20149  mcubic  20159  leibpi  20254  efrlim  20280  amgmlem  20300  basellem7  20340  basellem9  20342  vmaval  20367  prmorcht  20432  musum  20447  chtublem  20466  pclogsum  20470  logexprlim  20480  dchrbas  20490  dchrelbasd  20494  dchr1cl  20506  dchrabl  20509  dchrfi  20510  dchrptlem2  20520  dchrhash  20526  bposlem5  20543  bposlem6  20544  lgsfval  20556  lgsdir2lem5  20582  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgsquad2lem2  20614  2sqlem8  20627  2sqlem11  20630  chtppilimlem2  20639  chebbnd2  20642  chpchtlim  20644  chpo1ub  20645  vmadivsum  20647  rplogsumlem2  20650  rpvmasumlem  20652  dchrisum0re  20678  dchrisum0  20685  mudivsum  20695  selberglem1  20710  selberglem2  20711  selberg2lem  20715  selberg2  20716  pntrsumo1  20730  selbergr  20733  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  abvcxp  20780  grpodivfval  20925  gxfval  20940  isrngo  21061  dipfval  21291  ipval2  21296  lnoval  21346  ajfval  21403  minvecolem3  21471  h2hcau  21575  h2hlm  21576  opsqrlem3  22738  opsqrlem4  22739  ballotlemsval  23083  ballotlemieq  23091  itgeq12dv  23211  ofrn2  23222  off2  23223  fmptcof2  23244  cofmpt  23246  tpr2rico  23311  disjdifprg  23367  iundisjf  23380  lmdvglim  23392  gsumpropd2lem  23394  gsumconstf  23396  esumeq1  23432  esumeq2d  23434  esumc  23445  esumsplit  23446  esumcst  23451  esumsn  23452  esumpinfval  23456  esumcocn  23463  esummulc1  23464  hasheuni  23468  esumcvg  23469  ofcval  23475  ofcfn  23476  ofcfeqd2  23477  ofcf  23479  ofcfval4  23481  sigaval  23486  issgon  23499  sxval  23536  measvunilem0  23556  measvuni  23557  meascnbl  23561  itgmeq123dTMP  23604  itgmeq1dTMP  23605  itgmeq2dTMP  23606  itgmeq3dTMP  23607  indf1ofs  23624  totprobd  23644  probfinmeasb  23647  probmeasb  23648  orvcval4  23676  dstfrvclim1  23693  quartfull  23701  sconpi1  23785  cvmliftphtlem  23863  cvmlift3lem2  23866  eupath2lem2  23917  sinccvg  24021  circum  24022  relexp0  24040  relexpsucr  24041  rtrclreclem.subset  24057  rtrclreclem.min  24059  dfrtrcl2  24060  faclimlem3  24119  cbvcprod  24137  prodmolem2a  24157  zprod  24160  fprod  24164  prod1  24169  br8  24184  br4  24186  trpred0  24310  elno2  24379  brsegle  24803  hilbert1.1  24849  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  ibladdnclem  25007  itgaddnclem1  25009  itgaddnclem2  25010  itgaddnc  25011  iblabsnclem  25014  iblabsnc  25015  iblmulc2nc  25016  itgmulc2nclem1  25017  itgmulc2nclem2  25018  itgmulc2nc  25019  bddiblnc  25021  ftc1cnnclem  25024  areacirc  25034  eqfnung2  25221  fprg  25236  islatalg  25286  isoriso  25315  fsumprd  25432  fincmpzer  25453  ltrcmp  25508  vecval1b  25554  vecval3b  25555  vri  25595  islimrs  25683  isaddrv  25749  isnullcv  25755  valvze  25757  isucv  25780  ismulcv  25784  fnmulcv  25787  isdivcv2  25796  isder  25810  imonclem  25916  iepiclem  25926  isntr  25976  islimcat  25979  partarelt2  26000  isgraphmrph  26026  domcatfun  26028  domcatval  26033  codcatfun  26037  codcatval  26039  clscnc  26113  cndpv  26152  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  xsyysx  26248  isray  26257  trer  26330  tailfval  26424  unirep  26452  upixp  26506  sdc  26557  lmclim2  26577  geomcau  26578  caures  26579  caushft  26580  prdsbnd2  26622  heibor1lem  26636  bfplem2  26650  rrncmslem  26659  eldiophb  26939  eldioph  26940  eldioph3  26948  rabren3dioph  27001  pellqrexplicit  27065  rmxycomplete  27105  rmxynorm  27106  acongrep  27170  jm2.26a  27196  jm2.26  27198  fnwe2lem2  27251  fnwe2lem3  27252  aomclem5  27258  aomclem8  27262  dsmmval  27303  dsmmsubg  27312  imasgim  27367  isnumbasgrplem1  27369  islindf  27385  islindf4  27411  hbtlem5  27435  dgrsub2  27442  rgspnid  27480  rngunsnply  27481  pmtrval  27497  symgsssg  27511  symgfisg  27512  psgnunilem4  27523  psgnvalii  27535  mamufval  27546  mamuval  27547  mamudi  27564  mamudir  27565  mat0  27575  matinvg  27576  matlmod  27582  matrng  27583  matassa  27584  mdetfval  27590  mendval  27594  mendrng  27603  mendlmod  27604  mendassa  27605  caofcan  27643  ofsubid  27644  ofmul12  27645  ofdivrec  27646  ofdivcan4  27647  ofdivdiv2  27648  expgrowth  27655  fmuldfeqlem1  27815  clim1fr1  27830  climrec  27832  climexp  27834  climinf  27835  climsuse  27837  climneg  27839  stoweidlem2  27854  stoweidlem17  27869  stoweidlem21  27873  stoweidlem31  27883  stoweidlem32  27884  stoweidlem34  27886  stoweidlem44  27896  stoweidlem46  27898  stoweidlem55  27907  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem5  27930  stirlinglem6  27931  stirlinglem14  27939  afveq12d  28101  afveq1  28102  afveq2  28103  afvco2  28144  rspceaov  28165  ffnaov  28167  faovcl  28168  fzo0to3tp  28210  s2f1o  28223  s4f1o  28225  usgra0v  28251  usgra1v  28260  usgraexvlem  28261  nbgranself  28283  wlkonwlk  28334  constr3trllem2  28397  frgra3vlem1  28424  3vfriswmgralem  28428  lflset  29871  islfld  29874  lfladdcl  29883  lflvscl  29889  lkrsc  29909  eqlkr2  29912  lshpkrlem1  29922  ldualset  29937  ldualvaddval  29943  ldualvsval  29950  ldualgrplem  29957  lduallmodlem  29964  cmtfvalN  30022  isoml  30050  iscvlat  30135  llni2  30323  lplni2  30348  lvoli3  30388  lvoli2  30392  paddfval  30608  lhpset  30806  ltrnfset  30928  trlfset  30971  cdleme21k  31149  cdlemeiota  31396  tgrpfset  31555  tgrpset  31556  tgrpabl  31562  tendo0cbv  31597  tendo02  31598  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  cdlemk40  31728  cdlemkid5  31746  cdlemkid  31747  dvafset  31815  dvaset  31816  diaffval  31842  dialss  31858  diaf11N  31861  dvhfset  31892  dvhset  31893  docaffvalN  31933  dibfval  31953  dibf11N  31973  diblss  31982  diclss  32005  dihord2cN  32033  dihord11b  32034  dihffval  32042  dihord6apre  32068  dihglblem2aN  32105  dihglblem2N  32106  dihjatcclem4  32233  lclkrs  32351  mapdh6dN  32551  mapdh6eN  32552  mapdh6fN  32553  mapdh6jN  32557  hvmapffval  32570  hvmapfval  32571  mapdh8a  32587  mapdh8ad  32591  mapdh8d0N  32594  mapdh8d  32595  mapdh8i  32599  mapdh8j  32600  mapdh9a  32602  mapdh9aOLDN  32603  hdmap1l6d  32626  hdmap1l6e  32627  hdmap1l6f  32628  hdmap1l6j  32632  hdmapval2  32647  hdmapeveclem  32649  hdmapval3lemN  32652  hdmap11lem1  32656  hgmapfval  32701  hlhils0  32760  hlhils1N  32761  hlhillvec  32766  hlhildrng  32767  hlhil0  32770  hlhillsm  32771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator