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

Theorem eqidd 2405
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 2404 . 2  |-  A  =  A
21a1i 11 1  |-  ( ph  ->  A  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  nfabd2  2558  cbvraldva  2898  cbvrexdva  2899  nelrdva  3103  opeq1  3944  opeq2  3945  mpteq1  4249  nfcvb  4354  tfisi  4797  iotanul  5392  feq23d  5547  fvmptdv2  5777  elrnrexdm  5833  fmptco  5860  fprg  5874  ftpg  5875  fliftfun  5993  fliftval  5997  cbvmpt2  6110  eqfnov2  6136  ovmpt2d  6160  ovmpt2dv2  6166  ofval  6273  ofrval  6274  offn  6275  fnfvof  6276  off  6279  ofres  6280  ofco  6283  caofref  6289  caofid0l  6291  caofid0r  6292  caofid1  6293  caofid2  6294  caofrss  6296  caoftrn  6298  suppssof1  6305  riotabidv  6510  nfriotad  6517  iserd  6890  ixpsnf1o  7061  mapxpen  7232  dffi3  7394  oieq1  7437  oieq2  7438  cantnfp1  7593  cantnflem1d  7600  cantnflem1  7601  iunfictbso  7951  axcclem  8293  ttukeylem3  8347  ttukey2g  8352  fpwwe2lem9  8469  ofsubeq0  9953  ofnegsub  9954  ofsubge0  9955  fzo0to3tp  11140  seqeq2  11282  seqeq3  11283  seqid  11323  seqid2  11324  seqz  11326  seqof  11335  bcval  11550  swrdval  11719  wrdind  11746  s2f1o  11818  s4f1o  11820  rlim2  12245  climcl  12248  rlimcl  12252  clim2  12253  lo1o12  12282  rlimclim1  12294  rlimclim  12295  climrlim2  12296  climuni  12301  rlimres  12307  climeq  12316  2clim  12321  climshftlem  12323  climabs0  12334  rlimcn1b  12338  climcn1  12340  climcn2  12341  o1of2  12361  o1rlimmul  12367  o1add2  12372  o1mul2  12373  o1sub2  12374  o1dif  12378  climsqz  12389  climsqz2  12390  rlimdiv  12394  isercoll  12416  climsup  12418  climcau  12419  caurcvgr  12422  caucvgb  12428  serf0  12429  iseralt  12433  cbvsum  12444  summolem2a  12464  zsum  12467  fsum  12469  sumz  12471  sumss  12473  fsumss  12474  sumss2  12475  fsumcvg2  12476  fsumser  12479  isumclim3  12498  isummulc2  12501  fsum2dlem  12509  fsumconst  12528  fsumabs  12535  fsumparts  12540  fsumrlim  12545  fsumo1  12546  seqabs  12548  cvgcmpce  12552  fsumiun  12555  ackbijnn  12562  isumshft  12574  isumless  12580  isumltss  12583  climcndslem1  12584  climcndslem2  12585  climcnds  12586  mertenslem1  12616  mertenslem2  12617  eftlcl  12663  reeftlcl  12664  eftlub  12665  efsep  12666  effsumlt  12667  eirrlem  12758  rpnnen2lem1  12769  rpnnen2lem6  12774  rpnnen2lem7  12775  rpnnen2lem8  12776  rpnnen2lem9  12777  rpnnen2  12780  rpnnen  12781  sadadd2lem  12926  sadadd2  12927  sadasslem  12937  smupvallem  12950  smumul  12960  alginv  13021  algfx  13026  qnumdencoprm  13092  qeqnumdivden  13093  pcmpt  13216  pcmptdvds  13218  prmreclem2  13240  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  prmrec  13245  vdwlem1  13304  vdwlem12  13315  vdwlem13  13316  ramub1lem2  13350  ramcl  13352  prdssca  13634  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsle  13639  prdsds  13641  prdstset  13643  prdshom  13644  prdsco  13645  prdsvscafval  13657  prdsdsval2  13661  prdsdsval3  13662  pwsle  13669  pwsleval  13670  pwsvscaval  13672  imasbas  13693  imasds  13694  imasplusg  13698  imasmulr  13699  imassca  13700  imasvsca  13701  imastset  13702  imasle  13703  imasvscafn  13717  imasvscaval  13718  divsin  13724  xpsvsca  13759  iscat  13852  iscatd  13853  iscatd2  13861  0catg  13867  homfeq  13875  homfeqd  13876  comfffval2  13882  comffval2  13883  comfeq  13887  comfeqd  13888  oppccatid  13900  2oppccomf  13906  moni  13917  ssc2  13977  ssctr  13980  ssceq  13981  subcssc  13992  subccat  14000  subsubc  14005  funcres  14048  funcres2  14050  funcres2c  14053  idffth  14085  cofull  14086  cofth  14087  ressffth  14090  isnat  14099  fuccofval  14111  fuccatid  14121  fucpropd  14129  elhomai  14143  coafval  14174  setcval  14187  setcbas  14188  setchomfval  14189  setccofval  14192  setcco  14193  setccatid  14194  setcepi  14198  funcsetcres2  14203  catcval  14206  catcbas  14207  catchomfval  14208  catccofval  14210  catcco  14211  catccatid  14212  catciso  14217  catcfuccl  14219  xpcbas  14230  xpchomfval  14231  xpccofval  14234  xpccatid  14240  prfval  14251  catcxpccl  14259  xpcpropd  14260  evlfval  14269  curfval  14275  curf1  14277  curf12  14279  curf2  14281  curf2val  14282  hofval  14304  hof2fval  14307  hofcllem  14310  oppchofcl  14312  oppcyon  14321  oyoncl  14322  yonedalem4a  14327  yonedalem4b  14328  yonedalem4c  14329  yonedalem3b  14331  yonedainv  14333  oduposb  14518  ipopos  14541  isdlat  14574  ismnd  14647  ismndd  14674  mndprop  14678  prdsmndd  14683  imasmnd2  14687  gsumpropd  14731  gsumval1  14734  gsumval2a  14737  frmdbas  14752  frmdmnd  14759  grpprop  14779  grpsubfval  14802  grpsubpropd  14844  mulgfval  14846  mulgpropd  14878  prdsgrpd  14882  imasgrp2  14888  imasgrp  14889  imasgrpf1  14890  subgsub  14911  eqgfval  14943  divsgrp  14950  symgval  15049  symggrp  15058  oppgmnd  15105  oppgmndb  15106  oppggrp  15108  oppggrpb  15109  oppglsm  15231  lsmelvalmi  15241  efgi0  15307  efgi1  15308  efgtf  15309  efgval2  15311  efginvrel2  15314  frgp0  15347  frgpup3lem  15364  ablprop  15378  subcmn  15411  gex2abl  15421  prdscmnd  15431  divsabl  15435  cyggenod2  15450  cygabl  15455  gsumzf1o  15474  gsumzaddlem  15481  gsumzsplit  15484  gsumconst  15487  gsummhm2  15490  gsumunsn  15499  gsumpt  15500  gsum2d  15501  gsumcom2  15504  dprdval  15516  dprdssv  15529  dprdfeq0  15535  dprdsubg  15537  dprdspan  15540  dprdz  15543  subgdmdprd  15547  subgdprd  15548  dmdprdsplitlem  15550  isrng  15623  rngabl  15648  rngprop  15652  isrngd  15653  prdsrngd  15673  prdscrngd  15674  prds1  15675  imasrng  15680  opprrng  15691  opprrngb  15692  dvrfval  15744  pwsco1rhm  15788  pwsco2rhm  15789  drngprop  15801  isdrngd  15815  isdrngrd  15816  pwsdiagrhm  15856  abvtrivd  15883  islmodd  15911  lmodabl  15946  lss1  15970  lsssn0  15979  islss3  15990  lss1d  15994  lssintcl  15995  prdslmodd  16000  idlmhm  16072  invlmhm  16073  lmhmvsca  16076  lbsextlem2  16186  sralmod  16213  sralmod0  16214  rlm0  16224  rlmvneg  16233  crngridl  16264  divscrng  16266  isassa  16330  isassad  16337  issubassa  16338  sraassa  16339  asclfval  16348  ressascl  16357  psrval  16384  psrbaglesupp  16388  psrbagcon  16391  psrbaglefi  16392  psrbagconf1o  16394  gsumbagdiaglem  16395  psrass1lem  16397  psrbas  16398  psrplusg  16400  psrmulr  16403  psrsca  16408  psrvscafval  16409  psrvscaval  16411  psrgrp  16417  psrlmod  16420  psrlidm  16422  psrdi  16425  psrdir  16426  psrcom  16427  psrrng  16429  psrassa  16432  mplsubglem  16453  mpllsslem  16454  mplvscaval  16466  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  opsrcrng  16503  opsrassa  16504  mplmon2  16508  evlslem2  16523  ply1lss  16549  ply1subrg  16550  opsr0  16567  opsr1  16568  subrgply1  16582  psrplusgpropd  16584  psropprmul  16587  opsrrng  16594  opsrlmod  16595  ply1mpl0  16604  ply1mpl1  16605  coe1z  16611  coe1mul2  16617  coe1tm  16620  coe1tmmul2fv  16625  coe1pwmulfv  16627  coe1sclmulfv  16630  ply1coe  16639  absabv  16711  zrhpropd  16751  znzrh  16778  znbas  16779  zncrng  16780  znzrhfo  16783  znf1o  16787  cyggic  16808  frgpcyg  16809  isphld  16840  phlpropd  16841  pjfval  16888  epttop  17028  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  lmss  17316  2ndci  17464  2ndcsep  17475  dis2ndc  17476  1stcelcls  17477  ptbasid  17560  xkoopn  17574  prdstopn  17613  ptrescn  17624  txlm  17633  lmcn2  17634  tx1stc  17635  xkopt  17640  cnmpt2c  17655  cnmptk1  17666  cnmpt1k  17667  cnmptkk  17668  qtopeu  17701  txswaphmeolem  17789  xpstopnlem1  17794  ptcmpfi  17798  xkohmeo  17800  rnelfmlem  17937  rnelfm  17938  hauspwpwf1  17972  lmflf  17990  flfcnp2  17992  fclsval  17993  alexsubb  18030  tmdgsum  18078  tgpconcomp  18095  divstgphaus  18105  tsmsfbas  18110  tsmspropd  18114  tsms0  18124  tsmsmhm  18128  tgptsmscls  18132  tsmssplit  18134  tsmsxplem1  18135  tsmsxplem2  18136  ustuqtop4  18227  imasdsf1olem  18356  blfvalps  18366  stdbdmetval  18497  stdbdxmet  18498  met2ndci  18505  prdsxmslem2  18512  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  nmfval  18589  nmpropd  18594  nmpropd2  18595  subgnm  18627  tng0  18637  tngnm  18645  tngnrg  18663  sranlm  18673  qdensere  18757  fsumcn  18853  cncfmpt1f  18896  negfcncf  18902  oprpiece1res2  18930  htpyid  18955  phtpyid  18967  pcofval  18988  pcopt2  19001  om1bas  19009  om1plusg  19012  om1tset  19013  pi1bas  19016  pi1bas2  19019  pi1eluni  19020  pi1bas3  19021  pi1cpbl  19022  pi1addf  19025  pi1addval  19026  pi1grplem  19027  pi1xfr  19033  pi1xfrcnvlem  19034  pi1coghm  19039  cphassr  19127  tchphl  19138  ipcau2  19144  lmnn  19169  iscau  19182  cmetcaulem  19194  iscmet3lem1  19197  causs  19204  lmclim  19208  srabn  19267  ovollb2lem  19337  ovolfiniun  19350  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  shftmbl  19386  volfiniun  19394  ioombl1lem4  19408  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  vitalilem4  19456  ismbfcn2  19484  mbfmulc2lem  19492  mbfmulc2re  19493  mbfneg  19495  mbfposb  19498  mbfaddlem  19505  mbfadd  19506  mbfsub  19507  mbfmulc2  19508  0plef  19517  0pledm  19518  itg1ge0  19531  i1faddlem  19538  i1fmullem  19539  i1fmulclem  19547  itg1mulc  19549  i1fres  19550  i1fposd  19552  itg1lea  19557  itg1le  19558  itg1climres  19559  mbfi1fseqlem2  19561  mbfi1fseq  19566  mbfi1flimlem  19567  mbfi1flim  19568  mbfmullem2  19569  mbfmul  19571  xrge0f  19576  itg2ge0  19580  itg2const  19585  itg2const2  19586  itg2uba  19588  itg2lea  19589  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  isibl  19610  isibl2  19611  iblitg  19613  dfitg  19614  cbvitg  19620  itgeq2  19622  itgcl  19628  itgvallem  19629  ibl0  19631  iblcnlem1  19632  itgcnlem  19634  iblneg  19647  itgneg  19648  iblss  19649  iblss2  19650  i1fibl  19652  itgitg1  19653  itgle  19654  itgeqa  19658  itgss3  19659  iblconst  19662  ibladdlem  19664  ibladd  19665  itgaddlem1  19667  itgfsum  19671  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  itgsplit  19680  bddmulibl  19683  bddibl  19684  itgcn  19687  limccnp  19731  limccnp2  19732  limcco  19733  dvidlem  19755  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvaddf  19781  dvcmulf  19784  dvcjbr  19788  dvexp  19792  dvmptadd  19799  dvmptmul  19800  dvmptcj  19807  dvmptco  19811  dvmptfsum  19812  dvcnvlem  19813  dvef  19817  rolle  19827  mvth  19829  dvlip  19830  dvlipcn  19831  lhop1lem  19850  itgsubstlem  19885  evlslem1  19889  evl1rhm  19902  evl1sca  19903  evl1expd  19911  deg1suble  19983  ply1divalg2  20014  uc1pmon1p  20027  q1pval  20029  r1pval  20032  elply2  20068  elplyr  20073  plypf1  20084  plyaddlem1  20085  coeeulem  20096  plyco  20113  coeaddlem  20120  coemulc  20126  dgradd2  20139  dgrsub  20143  dgrcolem1  20144  dgrcolem2  20145  dgrco  20146  ofmulrt  20152  plydivlem3  20165  plydivlem4  20166  plyrem  20175  iaa  20195  aareccl  20196  aannenlem2  20199  aaliou3lem3  20214  aaliou3lem7  20219  taylfval  20228  taylply2  20237  dvntaylp  20240  taylthlem2  20243  ulmclm  20256  ulmres  20257  ulmshftlem  20258  ulm0  20260  ulmcau  20264  ulmss  20266  ulmbdd  20267  ulmcn  20268  mtest  20273  mtestbdd  20274  iblulm  20276  itgulm  20277  pserulm  20291  pserdvlem2  20297  abelthlem5  20304  abelthlem6  20305  abelthlem8  20308  abelthlem9  20309  sincn  20313  coscn  20314  efcvx  20318  logfac  20448  logcn  20491  chordthmlem  20626  chordthmlem5  20630  mcubic  20640  leibpi  20735  efrlim  20761  amgmlem  20781  basellem7  20822  basellem9  20824  vmaval  20849  prmorcht  20914  musum  20929  chtublem  20948  pclogsum  20952  logexprlim  20962  dchrbas  20972  dchrelbasd  20976  dchr1cl  20988  dchrabl  20991  dchrfi  20992  dchrptlem2  21002  dchrhash  21008  bposlem5  21025  bposlem6  21026  lgsfval  21038  lgsdir2lem5  21064  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquad2lem2  21096  2sqlem8  21109  2sqlem11  21112  chtppilimlem2  21121  chebbnd2  21124  chpchtlim  21126  chpo1ub  21127  vmadivsum  21129  rplogsumlem2  21132  rpvmasumlem  21134  dchrisum0re  21160  dchrisum0  21167  mudivsum  21177  selberglem1  21192  selberglem2  21193  selberg2lem  21197  selberg2  21198  pntrsumo1  21212  selbergr  21215  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  abvcxp  21262  usgra0v  21344  usgra1v  21362  usgraexvlem  21367  usgrares1  21377  nbgranself  21399  cusgrafilem2  21442  wlkonwlk  21488  0pthon1  21533  constr3trllem2  21591  eupath2lem2  21653  grpodivfval  21783  gxfval  21798  isrngo  21919  dipfval  22151  ipval2  22156  lnoval  22206  ajfval  22263  minvecolem3  22331  h2hcau  22435  h2hlm  22436  opsqrlem3  23598  opsqrlem4  23599  disjdifprg  23970  iundisjf  23982  ofrn2  24006  off2  24007  ofresid  24008  fmptcof2  24029  cofmpt  24031  ofpreima  24034  ressnm  24137  abvpropd2  24138  gsumpropd2lem  24173  gsumconstf  24175  subofld  24198  inftmrel  24203  isinftm  24204  tpr2rico  24263  lmdvglim  24292  qqhval  24311  qqhval2  24319  rrhf  24334  xrhval  24337  indf1ofs  24376  esumeq1  24384  esumeq1d  24385  esumeq2d  24387  esumf1o  24398  esumsplit  24400  esumadd  24401  gsumesum  24404  esumlub  24405  esumaddf  24406  esumcst  24408  esumsn  24409  esumpinfval  24416  esumcocn  24423  esummulc1  24424  esumcvg  24429  ofcval  24435  ofcfn  24436  ofcfeqd2  24437  ofcf  24439  ofcfval4  24441  sxval  24497  measvunilem0  24520  measvuni  24521  measiun  24525  meascnbl  24526  measinb  24528  volmeas  24540  sxbrsiga  24593  itgeq12dv  24594  sitgval  24600  totprobd  24637  probfinmeasb  24640  probmeasb  24641  rrvadd  24663  orvcval4  24671  dstfrvclim1  24688  ballotlemsval  24719  ballotlemieq  24727  quartfull  24749  lgamgulmlem2  24767  lgamcvg2  24792  sconpi1  24879  cvmliftphtlem  24957  cvmlift3lem2  24960  sinccvg  25063  circum  25064  relexp0  25082  relexpsucr  25083  rtrclreclem.subset  25098  rtrclreclem.min  25100  dfrtrcl2  25101  cbvprod  25194  prodmolem2a  25213  zprod  25216  fprod  25220  fprodntriv  25221  prod1  25223  prodss  25226  fprodss  25227  fprodconst  25255  fprod2dlem  25257  iprodclim3  25266  br8  25327  br4  25329  trpred0  25453  elno2  25522  brsegle  25946  hilbert1.1  25992  mblfinlem  26143  volsupnfl  26150  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  itgaddnc  26164  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  itgmulc2nclem2  26171  itgmulc2nc  26172  bddiblnc  26174  ftc1cnnclem  26177  areacirc  26187  trer  26209  unirep  26304  upixp  26321  sdc  26338  lmclim2  26354  geomcau  26355  caures  26356  caushft  26357  prdsbnd2  26394  heibor1lem  26408  bfplem2  26422  rrncmslem  26431  eldiophb  26705  eldioph  26706  eldioph3  26714  rabren3dioph  26766  pellqrexplicit  26830  rmxycomplete  26870  rmxynorm  26871  acongrep  26935  jm2.26a  26961  jm2.26  26963  fnwe2lem2  27016  fnwe2lem3  27017  aomclem5  27023  aomclem8  27027  dsmmval  27068  dsmmsubg  27077  imasgim  27132  isnumbasgrplem1  27134  islindf  27150  islindf4  27176  hbtlem5  27200  dgrsub2  27207  rgspnid  27245  rngunsnply  27246  pmtrval  27262  symgsssg  27276  symgfisg  27277  psgnunilem4  27288  psgnvalii  27300  mamufval  27311  mamuval  27312  mamudi  27329  mamudir  27330  mat0  27340  matinvg  27341  matlmod  27347  matrng  27348  matassa  27349  mendval  27359  mendrng  27368  mendlmod  27369  mendassa  27370  caofcan  27408  ofsubid  27409  ofmul12  27410  ofdivrec  27411  ofdivcan4  27412  ofdivdiv2  27413  expgrowth  27420  clim1fr1  27594  climrec  27596  climexp  27598  climinf  27599  climsuse  27601  climneg  27603  stoweidlem2  27618  stoweidlem17  27633  stoweidlem21  27637  stoweidlem32  27648  stoweidlem46  27662  stoweidlem55  27671  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem3  27692  afveq12d  27864  afveq1  27865  afveq2  27866  afvco2  27907  rspceaov  27928  faovcl  27931  usgra2pthspth  28035  el2spthonot0  28068  2spontn0vne  28084  usg2spthonot1  28087  frgra3vlem1  28104  3vfriswmgralem  28108  frgrancvvdeqlem2  28134  frg2woteq  28163  usg2spot2nb  28168  usgreg2spot  28170  lflset  29542  islfld  29545  lfladdcl  29554  lflvscl  29560  lkrsc  29580  eqlkr2  29583  lshpkrlem1  29593  ldualset  29608  ldualvaddval  29614  ldualvsval  29621  ldualgrplem  29628  lduallmodlem  29635  cmtfvalN  29693  isoml  29721  iscvlat  29806  llni2  29994  lplni2  30019  lvoli3  30059  lvoli2  30063  paddfval  30279  lhpset  30477  ltrnfset  30599  trlfset  30642  cdleme21k  30820  cdlemeiota  31067  tgrpfset  31226  tgrpset  31227  tgrpabl  31233  tendo0cbv  31268  tendo02  31269  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  cdlemk40  31399  cdlemkid5  31417  cdlemkid  31418  dvafset  31486  dvaset  31487  diaffval  31513  dialss  31529  diaf11N  31532  dvhfset  31563  dvhset  31564  docaffvalN  31604  dibfval  31624  dibf11N  31644  diblss  31653  diclss  31676  dihord2cN  31704  dihord11b  31705  dihffval  31713  dihord6apre  31739  dihglblem2aN  31776  dihglblem2N  31777  dihjatcclem4  31904  lclkrs  32022  mapdh6dN  32222  mapdh6eN  32223  mapdh6fN  32224  mapdh6jN  32228  hvmapffval  32241  hvmapfval  32242  mapdh8a  32258  mapdh8ad  32262  mapdh8d0N  32265  mapdh8d  32266  mapdh8i  32270  mapdh8j  32271  mapdh9a  32273  mapdh9aOLDN  32274  hdmap1l6d  32297  hdmap1l6e  32298  hdmap1l6f  32299  hdmap1l6j  32303  hdmapval2  32318  hdmapeveclem  32320  hdmapval3lemN  32323  hdmap11lem1  32327  hgmapfval  32372  hlhils0  32431  hlhils1N  32432  hlhillvec  32437  hlhildrng  32438  hlhil0  32441  hlhillsm  32442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397
  Copyright terms: Public domain W3C validator