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

Theorem eqidd 2436
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 2435 . 2  |-  A  =  A
21a1i 11 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  nfabd2  2589  cbvraldva  2930  cbvrexdva  2931  nelrdva  3135  opeq1  3976  opeq2  3977  mpteq1  4281  nfcvb  4386  tfisi  4829  iotanul  5424  feq23d  5579  fvmptdv2  5809  elrnrexdm  5865  fmptco  5892  fprg  5906  ftpg  5907  fliftfun  6025  fliftval  6029  cbvmpt2  6142  eqfnov2  6168  ovmpt2d  6192  ovmpt2dv2  6198  ofval  6305  ofrval  6306  offn  6307  fnfvof  6308  off  6311  ofres  6312  ofco  6315  caofref  6321  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  caofrss  6328  caoftrn  6330  suppssof1  6337  riotabidv  6542  nfriotad  6549  iserd  6922  ixpsnf1o  7093  mapxpen  7264  dffi3  7427  oieq1  7470  oieq2  7471  cantnfp1  7626  cantnflem1d  7633  cantnflem1  7634  iunfictbso  7984  axcclem  8326  ttukeylem3  8380  ttukey2g  8385  fpwwe2lem9  8502  ofsubeq0  9986  ofnegsub  9987  ofsubge0  9988  fzo0to3tp  11173  seqeq2  11315  seqeq3  11316  seqid  11356  seqid2  11357  seqz  11359  seqof  11368  bcval  11583  swrdval  11752  wrdind  11779  s2f1o  11851  s4f1o  11853  rlim2  12278  climcl  12281  rlimcl  12285  clim2  12286  lo1o12  12315  rlimclim1  12327  rlimclim  12328  climrlim2  12329  climuni  12334  rlimres  12340  climeq  12349  2clim  12354  climshftlem  12356  climabs0  12367  rlimcn1b  12371  climcn1  12373  climcn2  12374  o1of2  12394  o1rlimmul  12400  o1add2  12405  o1mul2  12406  o1sub2  12407  o1dif  12411  climsqz  12422  climsqz2  12423  rlimdiv  12427  isercoll  12449  climsup  12451  climcau  12452  caurcvgr  12455  caucvgb  12461  serf0  12462  iseralt  12466  cbvsum  12477  summolem2a  12497  zsum  12500  fsum  12502  sumz  12504  sumss  12506  fsumss  12507  sumss2  12508  fsumcvg2  12509  fsumser  12512  isumclim3  12531  isummulc2  12534  fsum2dlem  12542  fsumconst  12561  fsumabs  12568  fsumparts  12573  fsumrlim  12578  fsumo1  12579  seqabs  12581  cvgcmpce  12585  fsumiun  12588  ackbijnn  12595  isumshft  12607  isumless  12613  isumltss  12616  climcndslem1  12617  climcndslem2  12618  climcnds  12619  mertenslem1  12649  mertenslem2  12650  eftlcl  12696  reeftlcl  12697  eftlub  12698  efsep  12699  effsumlt  12700  eirrlem  12791  rpnnen2lem1  12802  rpnnen2lem6  12807  rpnnen2lem7  12808  rpnnen2lem8  12809  rpnnen2lem9  12810  rpnnen2  12813  rpnnen  12814  sadadd2lem  12959  sadadd2  12960  sadasslem  12970  smupvallem  12983  smumul  12993  alginv  13054  algfx  13059  qnumdencoprm  13125  qeqnumdivden  13126  pcmpt  13249  pcmptdvds  13251  prmreclem2  13273  prmreclem4  13275  prmreclem5  13276  prmreclem6  13277  prmrec  13278  vdwlem1  13337  vdwlem12  13348  vdwlem13  13349  ramub1lem2  13383  ramcl  13385  prdssca  13667  prdsbas  13668  prdsplusg  13669  prdsmulr  13670  prdsvsca  13671  prdsle  13672  prdsds  13674  prdstset  13676  prdshom  13677  prdsco  13678  prdsvscafval  13690  prdsdsval2  13694  prdsdsval3  13695  pwsle  13702  pwsleval  13703  pwsvscaval  13705  imasbas  13726  imasds  13727  imasplusg  13731  imasmulr  13732  imassca  13733  imasvsca  13734  imastset  13735  imasle  13736  imasvscafn  13750  imasvscaval  13751  divsin  13757  xpsvsca  13792  iscat  13885  iscatd  13886  iscatd2  13894  0catg  13900  homfeq  13908  homfeqd  13909  comfffval2  13915  comffval2  13916  comfeq  13920  comfeqd  13921  oppccatid  13933  2oppccomf  13939  moni  13950  ssc2  14010  ssctr  14013  ssceq  14014  subcssc  14025  subccat  14033  subsubc  14038  funcres  14081  funcres2  14083  funcres2c  14086  idffth  14118  cofull  14119  cofth  14120  ressffth  14123  isnat  14132  fuccofval  14144  fuccatid  14154  fucpropd  14162  elhomai  14176  coafval  14207  setcval  14220  setcbas  14221  setchomfval  14222  setccofval  14225  setcco  14226  setccatid  14227  setcepi  14231  funcsetcres2  14236  catcval  14239  catcbas  14240  catchomfval  14241  catccofval  14243  catcco  14244  catccatid  14245  catciso  14250  catcfuccl  14252  xpcbas  14263  xpchomfval  14264  xpccofval  14267  xpccatid  14273  prfval  14284  catcxpccl  14292  xpcpropd  14293  evlfval  14302  curfval  14308  curf1  14310  curf12  14312  curf2  14314  curf2val  14315  hofval  14337  hof2fval  14340  hofcllem  14343  oppchofcl  14345  oppcyon  14354  oyoncl  14355  yonedalem4a  14360  yonedalem4b  14361  yonedalem4c  14362  yonedalem3b  14364  yonedainv  14366  oduposb  14551  ipopos  14574  isdlat  14607  ismnd  14680  ismndd  14707  mndprop  14711  prdsmndd  14716  imasmnd2  14720  gsumpropd  14764  gsumval1  14767  gsumval2a  14770  frmdbas  14785  frmdmnd  14792  grpprop  14812  grpsubfval  14835  grpsubpropd  14877  mulgfval  14879  mulgpropd  14911  prdsgrpd  14915  imasgrp2  14921  imasgrp  14922  imasgrpf1  14923  subgsub  14944  eqgfval  14976  divsgrp  14983  symgval  15082  symggrp  15091  oppgmnd  15138  oppgmndb  15139  oppggrp  15141  oppggrpb  15142  oppglsm  15264  lsmelvalmi  15274  efgi0  15340  efgi1  15341  efgtf  15342  efgval2  15344  efginvrel2  15347  frgp0  15380  frgpup3lem  15397  ablprop  15411  subcmn  15444  gex2abl  15454  prdscmnd  15464  divsabl  15468  cyggenod2  15483  cygabl  15488  gsumzf1o  15507  gsumzaddlem  15514  gsumzsplit  15517  gsumconst  15520  gsummhm2  15523  gsumunsn  15532  gsumpt  15533  gsum2d  15534  gsumcom2  15537  dprdval  15549  dprdssv  15562  dprdfeq0  15568  dprdsubg  15570  dprdspan  15573  dprdz  15576  subgdmdprd  15580  subgdprd  15581  dmdprdsplitlem  15583  isrng  15656  rngabl  15681  rngprop  15685  isrngd  15686  prdsrngd  15706  prdscrngd  15707  prds1  15708  imasrng  15713  opprrng  15724  opprrngb  15725  dvrfval  15777  pwsco1rhm  15821  pwsco2rhm  15822  drngprop  15834  isdrngd  15848  isdrngrd  15849  pwsdiagrhm  15889  abvtrivd  15916  islmodd  15944  lmodabl  15979  lss1  16003  lsssn0  16012  islss3  16023  lss1d  16027  lssintcl  16028  prdslmodd  16033  idlmhm  16105  invlmhm  16106  lmhmvsca  16109  lbsextlem2  16219  sralmod  16246  sralmod0  16247  rlm0  16257  rlmvneg  16266  crngridl  16297  divscrng  16299  isassa  16363  isassad  16370  issubassa  16371  sraassa  16372  asclfval  16381  ressascl  16390  psrval  16417  psrbaglesupp  16421  psrbagcon  16424  psrbaglefi  16425  psrbagconf1o  16427  gsumbagdiaglem  16428  psrass1lem  16430  psrbas  16431  psrplusg  16433  psrmulr  16436  psrsca  16441  psrvscafval  16442  psrvscaval  16444  psrgrp  16450  psrlmod  16453  psrlidm  16455  psrdi  16458  psrdir  16459  psrcom  16460  psrrng  16462  psrassa  16465  mplsubglem  16486  mpllsslem  16487  mplvscaval  16499  mplcoe1  16516  mplcoe3  16517  mplcoe2  16518  opsrcrng  16536  opsrassa  16537  mplmon2  16541  evlslem2  16556  ply1lss  16582  ply1subrg  16583  opsr0  16600  opsr1  16601  subrgply1  16615  psrplusgpropd  16617  psropprmul  16620  opsrrng  16627  opsrlmod  16628  ply1mpl0  16637  ply1mpl1  16638  coe1z  16644  coe1mul2  16650  coe1tm  16653  coe1tmmul2fv  16658  coe1pwmulfv  16660  coe1sclmulfv  16663  ply1coe  16672  absabv  16744  zrhpropd  16784  znzrh  16811  znbas  16812  zncrng  16813  znzrhfo  16816  znf1o  16820  cyggic  16841  frgpcyg  16842  isphld  16873  phlpropd  16874  pjfval  16921  epttop  17061  ordtbas2  17243  ordtopn1  17246  ordtopn2  17247  lmss  17350  2ndci  17499  2ndcsep  17510  dis2ndc  17511  1stcelcls  17512  ptbasid  17595  xkoopn  17609  prdstopn  17648  ptrescn  17659  txlm  17668  lmcn2  17669  tx1stc  17670  xkopt  17675  cnmpt2c  17690  cnmptk1  17701  cnmpt1k  17702  cnmptkk  17703  qtopeu  17736  txswaphmeolem  17824  xpstopnlem1  17829  ptcmpfi  17833  xkohmeo  17835  rnelfmlem  17972  rnelfm  17973  hauspwpwf1  18007  lmflf  18025  flfcnp2  18027  fclsval  18028  alexsubb  18065  tmdgsum  18113  tgpconcomp  18130  divstgphaus  18140  tsmsfbas  18145  tsmspropd  18149  tsms0  18159  tsmsmhm  18163  tgptsmscls  18167  tsmssplit  18169  tsmsxplem1  18170  tsmsxplem2  18171  ustuqtop4  18262  imasdsf1olem  18391  blfvalps  18401  stdbdmetval  18532  stdbdxmet  18533  met2ndci  18540  prdsxmslem2  18547  metustexhalfOLD  18581  metustexhalf  18582  cfilucfilOLD  18587  cfilucfil  18588  restmetu  18605  nmfval  18624  nmpropd  18629  nmpropd2  18630  subgnm  18662  tng0  18672  tngnm  18680  tngnrg  18698  sranlm  18708  qdensere  18792  fsumcn  18888  cncfmpt1f  18931  negfcncf  18937  oprpiece1res2  18965  htpyid  18990  phtpyid  19002  pcofval  19023  pcopt2  19036  om1bas  19044  om1plusg  19047  om1tset  19048  pi1bas  19051  pi1bas2  19054  pi1eluni  19055  pi1bas3  19056  pi1cpbl  19057  pi1addf  19060  pi1addval  19061  pi1grplem  19062  pi1xfr  19068  pi1xfrcnvlem  19069  pi1coghm  19074  cphassr  19162  tchphl  19173  ipcau2  19179  lmnn  19204  iscau  19217  cmetcaulem  19229  iscmet3lem1  19232  causs  19239  lmclim  19243  srabn  19302  ovollb2lem  19372  ovolfiniun  19385  ovolicc2lem3  19403  ovolicc2lem4  19404  ovolicc2lem5  19405  shftmbl  19421  volfiniun  19429  ioombl1lem4  19443  uniioombllem2  19463  uniioombllem3  19465  uniioombllem6  19468  vitalilem4  19491  ismbfcn2  19519  mbfmulc2lem  19527  mbfmulc2re  19528  mbfneg  19530  mbfposb  19533  mbfaddlem  19540  mbfadd  19541  mbfsub  19542  mbfmulc2  19543  0plef  19552  0pledm  19553  itg1ge0  19566  i1faddlem  19573  i1fmullem  19574  i1fmulclem  19582  itg1mulc  19584  i1fres  19585  i1fposd  19587  itg1lea  19592  itg1le  19593  itg1climres  19594  mbfi1fseqlem2  19596  mbfi1fseq  19601  mbfi1flimlem  19602  mbfi1flim  19603  mbfmullem2  19604  mbfmul  19606  xrge0f  19611  itg2ge0  19615  itg2const  19620  itg2const2  19621  itg2uba  19623  itg2lea  19624  itg2splitlem  19628  itg2split  19629  itg2monolem1  19630  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq  19635  itg2addlem  19638  itg2gt0  19640  itg2cnlem1  19641  itg2cnlem2  19642  itg2cn  19643  isibl  19645  isibl2  19646  iblitg  19648  dfitg  19649  cbvitg  19655  itgeq2  19657  itgcl  19663  itgvallem  19664  ibl0  19666  iblcnlem1  19667  itgcnlem  19669  iblneg  19682  itgneg  19683  iblss  19684  iblss2  19685  i1fibl  19687  itgitg1  19688  itgle  19689  itgeqa  19693  itgss3  19694  iblconst  19697  ibladdlem  19699  ibladd  19700  itgaddlem1  19702  itgfsum  19706  iblabslem  19707  iblabs  19708  iblabsr  19709  iblmulc2  19710  itgmulc2lem1  19711  itgsplit  19715  bddmulibl  19718  bddibl  19719  itgcn  19722  limccnp  19766  limccnp2  19767  limcco  19768  dvidlem  19790  dvcnp2  19794  dvaddbr  19812  dvmulbr  19813  dvaddf  19816  dvcmulf  19819  dvcjbr  19823  dvexp  19827  dvmptadd  19834  dvmptmul  19835  dvmptcj  19842  dvmptco  19846  dvmptfsum  19847  dvcnvlem  19848  dvef  19852  rolle  19862  mvth  19864  dvlip  19865  dvlipcn  19866  lhop1lem  19885  itgsubstlem  19920  evlslem1  19924  evl1rhm  19937  evl1sca  19938  evl1expd  19946  deg1suble  20018  ply1divalg2  20049  uc1pmon1p  20062  q1pval  20064  r1pval  20067  elply2  20103  elplyr  20108  plypf1  20119  plyaddlem1  20120  coeeulem  20131  plyco  20148  coeaddlem  20155  coemulc  20161  dgradd2  20174  dgrsub  20178  dgrcolem1  20179  dgrcolem2  20180  dgrco  20181  ofmulrt  20187  plydivlem3  20200  plydivlem4  20201  plyrem  20210  iaa  20230  aareccl  20231  aannenlem2  20234  aaliou3lem3  20249  aaliou3lem7  20254  taylfval  20263  taylply2  20272  dvntaylp  20275  taylthlem2  20278  ulmclm  20291  ulmres  20292  ulmshftlem  20293  ulm0  20295  ulmcau  20299  ulmss  20301  ulmbdd  20302  ulmcn  20303  mtest  20308  mtestbdd  20309  iblulm  20311  itgulm  20312  pserulm  20326  pserdvlem2  20332  abelthlem5  20339  abelthlem6  20340  abelthlem8  20343  abelthlem9  20344  sincn  20348  coscn  20349  efcvx  20353  logfac  20483  logcn  20526  chordthmlem  20661  chordthmlem5  20665  mcubic  20675  leibpi  20770  efrlim  20796  amgmlem  20816  basellem7  20857  basellem9  20859  vmaval  20884  prmorcht  20949  musum  20964  chtublem  20983  pclogsum  20987  logexprlim  20997  dchrbas  21007  dchrelbasd  21011  dchr1cl  21023  dchrabl  21026  dchrfi  21027  dchrptlem2  21037  dchrhash  21043  bposlem5  21060  bposlem6  21061  lgsfval  21073  lgsdir2lem5  21099  lgsdir  21102  lgsdilem2  21103  lgsdi  21104  lgsne0  21105  lgseisenlem2  21122  lgseisenlem3  21123  lgseisenlem4  21124  lgsquad2lem2  21131  2sqlem8  21144  2sqlem11  21147  chtppilimlem2  21156  chebbnd2  21159  chpchtlim  21161  chpo1ub  21162  vmadivsum  21164  rplogsumlem2  21167  rpvmasumlem  21169  dchrisum0re  21195  dchrisum0  21202  mudivsum  21212  selberglem1  21227  selberglem2  21228  selberg2lem  21232  selberg2  21233  pntrsumo1  21247  selbergr  21250  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  abvcxp  21297  usgra0v  21379  usgra1v  21397  usgraexvlem  21402  usgrares1  21412  nbgranself  21434  cusgrafilem2  21477  wlkonwlk  21523  0pthon1  21568  constr3trllem2  21626  eupath2lem2  21688  grpodivfval  21818  gxfval  21833  isrngo  21954  dipfval  22186  ipval2  22191  lnoval  22241  ajfval  22298  minvecolem3  22366  h2hcau  22470  h2hlm  22471  opsqrlem3  23633  opsqrlem4  23634  disjdifprg  24005  iundisjf  24017  ofrn2  24041  off2  24042  ofresid  24043  fmptcof2  24064  cofmpt  24066  ofpreima  24069  ressnm  24172  abvpropd2  24173  gsumpropd2lem  24208  gsumconstf  24210  subofld  24233  inftmrel  24238  isinftm  24239  tpr2rico  24298  lmdvglim  24327  qqhval  24346  qqhval2  24354  rrhf  24369  xrhval  24372  indf1ofs  24411  esumeq1  24419  esumeq1d  24420  esumeq2d  24422  esumf1o  24433  esumsplit  24435  esumadd  24436  gsumesum  24439  esumlub  24440  esumaddf  24441  esumcst  24443  esumsn  24444  esumpinfval  24451  esumcocn  24458  esummulc1  24459  esumcvg  24464  ofcval  24470  ofcfn  24471  ofcfeqd2  24472  ofcf  24474  ofcfval4  24476  sxval  24532  measvunilem0  24555  measvuni  24556  measiun  24560  meascnbl  24561  measinb  24563  volmeas  24575  sxbrsiga  24628  itgeq12dv  24629  sitgval  24635  totprobd  24672  probfinmeasb  24675  probmeasb  24676  rrvadd  24698  orvcval4  24706  dstfrvclim1  24723  ballotlemsval  24754  ballotlemieq  24762  quartfull  24784  lgamgulmlem2  24802  lgamcvg2  24827  sconpi1  24914  cvmliftphtlem  24992  cvmlift3lem2  24995  sinccvg  25098  circum  25099  relexp0  25117  relexpsucr  25118  rtrclreclem.subset  25133  rtrclreclem.min  25135  dfrtrcl2  25136  cbvprod  25230  prodmolem2a  25249  zprod  25252  fprod  25256  fprodntriv  25257  prod1  25259  prodss  25262  fprodss  25263  fprodconst  25291  fprod2dlem  25293  iprodclim3  25302  br8  25368  br4  25370  trpred0  25494  elno2  25563  brsegle  25990  hilbert1.1  26036  mblfinlem  26190  volsupnfl  26197  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  ibladdnclem  26207  itgaddnclem1  26209  itgaddnc  26211  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  itgmulc2nclem1  26217  itgmulc2nclem2  26218  itgmulc2nc  26219  bddiblnc  26221  ftc1cnnclem  26224  areacirc  26234  trer  26256  unirep  26351  upixp  26368  sdc  26385  lmclim2  26401  geomcau  26402  caures  26403  caushft  26404  prdsbnd2  26441  heibor1lem  26455  bfplem2  26469  rrncmslem  26478  eldiophb  26752  eldioph  26753  eldioph3  26761  rabren3dioph  26813  pellqrexplicit  26877  rmxycomplete  26917  rmxynorm  26918  acongrep  26982  jm2.26a  27008  jm2.26  27010  fnwe2lem2  27063  fnwe2lem3  27064  aomclem5  27070  aomclem8  27074  dsmmval  27115  dsmmsubg  27124  imasgim  27179  isnumbasgrplem1  27181  islindf  27197  islindf4  27223  hbtlem5  27247  dgrsub2  27254  rgspnid  27292  rngunsnply  27293  pmtrval  27309  symgsssg  27323  symgfisg  27324  psgnunilem4  27335  psgnvalii  27347  mamufval  27358  mamuval  27359  mamudi  27376  mamudir  27377  mat0  27387  matinvg  27388  matlmod  27394  matrng  27395  matassa  27396  mendval  27406  mendrng  27415  mendlmod  27416  mendassa  27417  caofcan  27455  ofsubid  27456  ofmul12  27457  ofdivrec  27458  ofdivcan4  27459  ofdivdiv2  27460  expgrowth  27467  clim1fr1  27641  climrec  27643  climexp  27645  climinf  27646  climsuse  27648  climneg  27650  stoweidlem2  27665  stoweidlem17  27680  stoweidlem21  27684  stoweidlem32  27695  stoweidlem46  27709  stoweidlem55  27718  wallispi  27733  wallispi2lem1  27734  wallispi2lem2  27735  wallispi2  27736  stirlinglem3  27739  afveq12d  27911  afveq1  27912  afveq2  27913  afvco2  27954  rspceaov  27975  faovcl  27978  modsubmod  28061  shwrdeqdifid  28158  shwrdssizelem1  28166  usgra2pthspth  28179  el2spthonot0  28212  2spontn0vne  28228  usg2spthonot1  28231  frgra3vlem1  28248  3vfriswmgralem  28252  frgrancvvdeqlem2  28278  frg2woteq  28307  usg2spot2nb  28312  usgreg2spot  28314  lflset  29696  islfld  29699  lfladdcl  29708  lflvscl  29714  lkrsc  29734  eqlkr2  29737  lshpkrlem1  29747  ldualset  29762  ldualvaddval  29768  ldualvsval  29775  ldualgrplem  29782  lduallmodlem  29789  cmtfvalN  29847  isoml  29875  iscvlat  29960  llni2  30148  lplni2  30173  lvoli3  30213  lvoli2  30217  paddfval  30433  lhpset  30631  ltrnfset  30753  trlfset  30796  cdleme21k  30974  cdlemeiota  31221  tgrpfset  31380  tgrpset  31381  tgrpabl  31387  tendo0cbv  31422  tendo02  31423  erngfset  31435  erngset  31436  erngfset-rN  31443  erngset-rN  31444  cdlemk40  31553  cdlemkid5  31571  cdlemkid  31572  dvafset  31640  dvaset  31641  diaffval  31667  dialss  31683  diaf11N  31686  dvhfset  31717  dvhset  31718  docaffvalN  31758  dibfval  31778  dibf11N  31798  diblss  31807  diclss  31830  dihord2cN  31858  dihord11b  31859  dihffval  31867  dihord6apre  31893  dihglblem2aN  31930  dihglblem2N  31931  dihjatcclem4  32058  lclkrs  32176  mapdh6dN  32376  mapdh6eN  32377  mapdh6fN  32378  mapdh6jN  32382  hvmapffval  32395  hvmapfval  32396  mapdh8a  32412  mapdh8ad  32416  mapdh8d0N  32419  mapdh8d  32420  mapdh8i  32424  mapdh8j  32425  mapdh9a  32427  mapdh9aOLDN  32428  hdmap1l6d  32451  hdmap1l6e  32452  hdmap1l6f  32453  hdmap1l6j  32457  hdmapval2  32472  hdmapeveclem  32474  hdmapval3lemN  32477  hdmap11lem1  32481  hgmapfval  32526  hlhils0  32585  hlhils1N  32586  hlhillvec  32591  hlhildrng  32592  hlhil0  32595  hlhillsm  32596
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428
  Copyright terms: Public domain W3C validator