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

Theorem eqcomi 2300
Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcomi.1  |-  A  =  B
Assertion
Ref Expression
eqcomi  |-  B  =  A

Proof of Theorem eqcomi
StepHypRef Expression
1 eqcomi.1 . 2  |-  A  =  B
2 eqcom 2298 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 199 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  eqtr2i  2317  eqtr3i  2318  eqtr4i  2319  syl5eqr  2342  syl5reqr  2343  syl6eqr  2346  syl6reqr  2347  eqeltrri  2367  eleqtrri  2369  syl5eqelr  2381  syl6eleqr  2387  abid2  2413  abid2f  2457  eqnetrri  2478  neeqtrri  2482  eqsstr3i  3222  sseqtr4i  3224  syl5eqssr  3236  syl6sseqr  3238  inrab2  3454  opid  3830  eqbrtrri  4060  breqtrri  4064  syl6breqr  4079  pwin  4313  unizlim  4525  orduniss2  4640  limon  4643  orduninsuc  4650  tfis  4661  dfdm2  5220  cnvresid  5338  fores  5476  funcoeqres  5520  fsnunres  5737  soisores  5840  fo1st  6155  fo2nd  6156  1st2val  6161  2nd2val  6162  cnvf1olem  6232  riotaprop  6344  riotaund  6357  seqomlem1  6478  om0r  6554  ixpsnf1o  6872  sbthlem5  6991  fodomr  7028  phplem4  7059  dif1enOLD  7106  dif1en  7107  fodomfi  7151  mapfien  7415  r1suc  7458  rankval4  7555  dif1card  7654  cardnum  7737  fin1a2lem13  8054  itunisuc  8061  ituniiun  8064  ttukeylem4  8155  alephval2  8210  recmulnq  8604  1lt2nq  8613  ltexnq  8615  mul02lem1  9004  addid1  9008  1p1e2  9856  2p1e3  9863  3p1e4  9864  4p1e5  9865  5p1e6  9866  6p1e7  9867  7p1e8  9868  8p1e9  9869  9p1e10  9870  zeo  10113  num0u  10149  numsucc  10166  1e0p1  10168  nummac  10172  6p5lem  10189  5t5e25  10216  6t6e36  10221  8t6e48  10232  decbin3  10245  fseq1p1m1  10873  expneg  11127  faclbnd4lem1  11322  eqs1  11463  s0s1  11565  imi  11658  abs1m  11835  caucvg  12167  sum2id  12197  incexclem  12311  incexc  12312  efsep  12406  pockthi  12970  dec2dvds  13094  1259prm  13150  2503prm  13154  4001prm  13159  homffval  13610  xpchomfval  13969  xpccofval  13972  yonedalem3b  14069  oduposb  14256  oduglb  14259  odulub  14261  psssdm2  14340  letsr  14365  gsumwspan  14484  mulgpropd  14616  odlem1  14866  gexlem1  14906  sylow2a  14946  oppglsm  14969  0frgp  15104  ablfac1eu  15324  prdsmgp  15409  pwsmgp  15417  isrhm  15517  drngui  15534  abvtrivd  15621  rlmval  15961  opsrbaslem  16235  psr1val  16281  ply1plusgfvi  16336  cnfld0  16414  cnfld1  16415  cnfldplusf  16417  xrge0cmn  16429  gzrngunit  16453  zzngim  16522  istpsi  16698  distopon  16750  indislem  16753  indistps2ALT  16767  distps  16768  discld  16842  restcls  16927  restntr  16928  dishaus  17126  discmp  17141  cmpsub  17143  2ndcsep  17201  txbas  17278  txdis  17342  txdis1cn  17345  txkgen  17362  xkopt  17365  xkofvcn  17394  hmphdis  17503  hmphindis  17504  txhmeo  17510  txswaphmeolem  17511  xpstopnlem1  17516  ptcmpfi  17520  tmdgsum  17794  symgtgp  17800  imasdsf1olem  17953  nrginvrcn  18218  idnghm  18268  xrsmopn  18334  zcld2  18337  metnrmlem2  18380  dfii3  18403  cncfcn1  18430  cncfmpt2f  18434  cdivcncf  18436  abscncfALT  18439  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  cnrehmeo  18467  lebnumii  18480  pcoass  18538  clmzlmvsca  18610  cncmet  18760  itg2cnlem2  19133  iblcnlem1  19158  itgcnlem  19160  limcdif  19242  cnlimc  19254  dvidlem  19281  dvcnp2  19285  dvcn  19286  dvnres  19296  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvexp  19318  dvrec  19320  dvexp3  19341  dveflem  19342  dvlipcn  19357  lhop1lem  19376  ftc1cn  19406  mpff  19441  deg1fvi  19487  dgrlt  19663  dgradd2  19665  coecj  19675  dvply1  19680  plyremlem  19700  aalioulem2  19729  dvtaylp  19765  taylthlem2  19769  psercn  19818  pserdvlem2  19820  pserdv  19821  abelth  19833  sinq34lt0t  19893  sincos6thpi  19899  efifo  19925  eff1olem  19926  loge  19956  logcn  20010  dvloglem  20011  dvlog  20014  dvlog2  20016  efopnlem2  20020  logtayl  20023  logccv  20026  cxpsqrlem  20065  cxpcn  20101  cxpcn2  20102  cxpcn3  20104  resqrcn  20105  sqrcn  20106  dvatan  20247  birthday  20265  divsqrsumlem  20290  emgt0  20316  ftalem3  20328  basellem5  20338  cht2  20426  cht3  20427  chtublem  20466  chtub  20467  logfacbnd3  20478  logexprlim  20480  dchr1cl  20506  dchrinvcl  20508  dchrfi  20510  dchrinv  20516  bclbnd  20535  bposlem6  20544  bposlem8  20546  lgsdir2lem2  20579  lgsdir  20585  2sqlem9  20628  2sqlem10  20629  dchrisum0flblem1  20673  logdivsum  20698  log2sumbnd  20709  ostth2  20802  ostth  20804  ex-dif  20826  1p1e2apr1  20855  isgrpoi  20881  grpofo  20882  0ngrp  20894  grpo2grp  20917  isass  20999  ismgm  21003  gidsn  21031  ginvsn  21032  rngosn  21087  rngoueqz  21113  bafval  21176  nvdm  21243  nvtri  21252  nmcnc  21285  cnbn  21464  hvsubcan2i  21659  normlem1  21705  normlem2  21706  bcseqi  21715  normpar2i  21751  hhnv  21760  hhssabloi  21855  hhshsslem1  21860  hhssvs  21865  hhsscms  21872  shscli  21912  ococi  22000  qlax1i  22222  qlaxr1i  22227  hosd1i  22418  nmcexi  22622  pjin1i  22788  hatomistici  22958  addltmulALT  23042  ballotth  23112  fmptpr  23229  tpr2uni  23303  rmulccn  23316  xrge0iifhmeo  23333  xrge0pluscn  23337  xrge0mulc1cn  23338  xrge0topn  23340  xrge0tmdALT  23342  esumnul  23442  esum0  23443  esumpfinval  23458  esumpfinvalf  23459  esumpcvgval  23461  zetacvg  23704  cprod2id  24150  prod2id  24170  setinds  24205  bdayfo  24400  fobigcup  24511  unisnif  24535  fullfunfnv  24556  axlowdimlem13  24654  fsumcube  24867  ordtoplem  24946  onsucconi  24948  onsucsuccmpi  24954  limsucncmpi  24956  ordcmp  24958  itg2addnclem  25003  itg2addnc  25005  itgaddnclem2  25010  ftc1cnnc  25025  oprabex2gpop  25139  isunscov  25177  mapex2  25243  2eq3m1  25282  islatalg  25286  isorhom  25314  isoriso  25315  toplat  25393  clfsebsr  25452  com2i  25519  vecval1b  25554  vecval3b  25555  vecax4  25559  vecax5  25560  mulveczer  25582  mulinvsca  25583  muldisc  25584  svli2  25587  osneisi  25634  intopcoaconlem3  25642  intopcoaconc  25644  usptop  25653  islimrs4  25685  bwt2  25695  flfneic  25727  tcnvec  25793  isdivcv2  25796  isder  25810  1alg  25825  algi  25830  dedi  25840  1ded  25841  dmrngcmp  25854  cati  25858  0alg  25859  1cat  25862  dmo  25879  cmpmorp  25882  mrdmcd  25897  homib  25899  cmphmia  25901  cmphmib  25902  iri  25903  ismona  25912  idmon  25920  isepia  25922  idsubidsup  25960  isinob  25965  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  prismorcsetlemc  26020  prismorcset2  26021  domcatfun  26028  codcatfun  26037  cmp2morpgrp  26066  cmpmorass  26069  morexcmp  26070  pgapspf  26155  bisig0  26165  isibg2  26213  sgplpte21  26235  sgplpte22  26241  nds  26253  isray  26257  isside0  26267  aishp  26275  isibcg  26294  ivthALT  26361  locfindis  26408  imaiinfv  26862  eldioph2  26944  elpell1qr2  27060  aomclem4  27257  kelac2  27266  islmodfg  27270  lmhmlnmsplit  27288  pwssplit4  27294  dsmmval2  27305  frlmsslss  27347  pwfi2f1o  27363  islindf4  27411  dgrsub2  27442  mamuvs1  27566  mamuvs2  27567  cytpval  27631  sbeqal2i  27702  compneOLD  27746  stoweidlem17  27869  stoweidlem26  27878  stoweidlem34  27886  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem1  27926  stirlinglem5  27930  stirlinglem8  27933  stirlinglem14  27939  funresfunco  28093  dfafv2  28100  ndmaovcl  28171  ndmaovcom  28173  f1oprg  28186  f1oun2prg  28187  fzo0to42pr  28211  usgraexvlem  28261  nb3graprlem2  28288  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  0wlk  28343  0trl  28344  wlkntrllem1  28345  wlkntrllem3  28347  wlkntrllem5  28349  0crct  28371  0cycl  28372  constr3trllem3  28398  constr3pthlem1  28401  constr3pthlem3  28403  frgra3v  28426  relopabVD  28993  bnj601  29268  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator