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

Theorem eqcomi 2408
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 2406 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 200 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  eqtr2i  2425  eqtr3i  2426  eqtr4i  2427  syl5eqr  2450  syl5reqr  2451  syl6eqr  2454  syl6reqr  2455  eqeltrri  2475  eleqtrri  2477  syl5eqelr  2489  syl6eleqr  2495  abid2  2521  abid2f  2565  eqnetrri  2586  neeqtrri  2590  eqsstr3i  3339  sseqtr4i  3341  syl5eqssr  3353  syl6sseqr  3355  difdif2  3558  inrab2  3574  opid  3962  eqbrtrri  4193  breqtrri  4197  syl6breqr  4212  pwin  4447  unizlim  4657  orduniss2  4772  limon  4775  orduninsuc  4782  tfis  4793  dfdm2  5360  cnvresid  5482  fores  5621  funcoeqres  5665  f1oprg  5677  fsnunres  5893  soisores  6006  fo1st  6325  fo2nd  6326  1st2val  6331  2nd2val  6332  cnvf1olem  6403  riotaprop  6532  riotaund  6545  seqomlem1  6666  om0r  6742  ixpsnf1o  7061  sbthlem5  7180  fodomr  7217  phplem4  7248  dif1enOLD  7299  dif1en  7300  fodomfi  7344  mapfien  7609  r1suc  7652  rankval4  7749  dif1card  7848  cardnum  7931  fin1a2lem13  8248  itunisuc  8255  ituniiun  8258  ttukeylem4  8348  alephval2  8403  recmulnq  8797  1lt2nq  8806  ltexnq  8808  mul02lem1  9198  addid1  9202  1p1e2  10050  3m1e2OLD  10053  2p1e3  10059  3p1e4  10060  4p1e5  10061  5p1e6  10062  6p1e7  10063  7p1e8  10064  8p1e9  10065  9p1e10  10066  zeo  10311  num0u  10347  numsucc  10364  1e0p1  10366  nummac  10370  6p5lem  10387  5t5e25  10414  6t6e36  10419  8t6e48  10430  decbin3  10443  fz0tp  11059  1fv  11075  fseq1p1m1  11077  fzo0to42pr  11141  expneg  11344  faclbnd4lem1  11539  bcn2m1  11570  bcn2p1  11571  hash2pr  11642  eqs1  11716  f1oun2prg  11819  s0s1  11824  imi  11917  abs1m  12094  caucvg  12427  sum2id  12457  incexclem  12571  incexc  12572  efsep  12666  pockthi  13230  dec2dvds  13354  1259prm  13410  2503prm  13414  4001prm  13419  homffval  13872  xpchomfval  14231  xpccofval  14234  yonedalem3b  14331  oduposb  14518  oduglb  14521  odulub  14523  psssdm2  14602  letsr  14627  gsumwspan  14746  mulgpropd  14878  odlem1  15128  gexlem1  15168  sylow2a  15208  oppglsm  15231  0frgp  15366  ablfac1eu  15586  prdsmgp  15671  pwsmgp  15679  isrhm  15779  drngui  15796  abvtrivd  15883  rlmval  16219  opsrbaslem  16493  psr1val  16539  ply1plusgfvi  16591  cnfld0  16680  cnfld1  16681  cnfldplusf  16683  xrge0cmn  16695  gzrngunit  16719  zzngim  16788  istpsi  16964  distopon  17016  indislem  17019  indistps2ALT  17033  distps  17034  discld  17108  restcls  17199  restntr  17200  dishaus  17400  discmp  17415  cmpsub  17417  2ndcsep  17475  txbas  17552  txdis  17617  txdis1cn  17620  txkgen  17637  xkopt  17640  xkofvcn  17669  hmphdis  17781  hmphindis  17782  txhmeo  17788  txswaphmeolem  17789  xpstopnlem1  17794  ptcmpfi  17798  tmdgsum  18078  symgtgp  18084  fmucndlem  18274  cuspcvg  18284  imasdsf1olem  18356  nrginvrcn  18680  idnghm  18730  xrsmopn  18796  zcld2  18799  metnrmlem2  18843  dfii3  18866  cncfcn1  18893  cncfmpt2f  18897  cdivcncf  18900  abscncfALT  18903  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  cnrehmeo  18931  lebnumii  18944  pcoass  19002  clmzlmvsca  19074  cncmet  19228  cnflduss  19263  itg2cnlem2  19607  iblcnlem1  19632  itgcnlem  19634  limcdif  19716  cnlimc  19728  dvidlem  19755  dvcnp2  19759  dvcn  19760  dvnres  19770  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvcjbr  19788  dvexp  19792  dvrec  19794  dvexp3  19815  dveflem  19816  dvlipcn  19831  lhop1lem  19850  ftc1cn  19880  mpff  19915  deg1fvi  19961  dgrlt  20137  dgradd2  20139  coecj  20149  dvply1  20154  plyremlem  20174  aalioulem2  20203  dvtaylp  20239  taylthlem2  20243  psercn  20295  pserdvlem2  20297  pserdv  20298  abelth  20310  sinq34lt0t  20370  sincos6thpi  20376  efifo  20402  eff1olem  20403  loge  20434  logcn  20491  dvloglem  20492  dvlog  20495  dvlog2  20497  efopnlem2  20501  logtayl  20504  logccv  20507  cxpsqrlem  20546  cxpcn  20582  cxpcn2  20583  cxpcn3  20585  resqrcn  20586  sqrcn  20587  dvatan  20728  birthday  20746  divsqrsumlem  20771  emgt0  20798  ftalem3  20810  basellem5  20820  cht2  20908  cht3  20909  chtublem  20948  logfacbnd3  20960  logexprlim  20962  dchr1cl  20988  dchrinvcl  20990  dchrfi  20992  dchrinv  20998  bclbnd  21017  bposlem6  21026  bposlem8  21028  lgsdir2lem2  21061  lgsdir  21067  2sqlem9  21110  2sqlem10  21111  dchrisum0flblem1  21155  logdivsum  21180  log2sumbnd  21191  ostth2  21284  ostth  21286  ausisusgra  21333  usgraexvlem  21367  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgraexilem2  21429  0wlk  21498  0trl  21499  2trllemE  21506  wlkntrllem1  21512  wlkntrllem3  21514  constr1trl  21541  0crct  21566  0cycl  21567  constr3trllem3  21592  ex-dif  21684  1p1e2apr1  21713  isgrpoi  21739  grpofo  21740  0ngrp  21752  grpo2grp  21775  isass  21857  ismgm  21861  gidsn  21889  ginvsn  21890  rngosn  21945  rngoueqz  21971  bafval  22036  nvdm  22103  nvtri  22112  nmcnc  22145  cnbn  22324  hvsubcan2i  22519  normlem1  22565  normlem2  22566  bcseqi  22575  normpar2i  22611  hhnv  22620  hhssabloi  22715  hhshsslem1  22720  hhssvs  22725  hhsscms  22732  shscli  22772  ococi  22860  qlax1i  23082  qlaxr1i  23087  hosd1i  23278  nmcexi  23482  pjin1i  23648  hatomistici  23818  addltmulALT  23902  fmptpr  24015  rhmopp  24210  tpr2uni  24256  rmulccn  24267  xrge0iifhmeo  24275  xrge0pluscn  24279  xrge0mulc1cn  24280  xrge0topn  24282  xrge0tmdOLD  24284  rezh  24308  qqh0  24321  qqh1  24322  rrhval  24332  rrhcn  24333  esumnul  24396  esum0  24397  esumpfinval  24418  esumpfinvalf  24419  esumpcvgval  24421  sitmval  24614  sitmcl  24616  ballotth  24748  zetacvg  24752  ntrivcvg  25178  prod2id  25207  fproddiv  25238  fprodfac  25249  fprodabs  25250  fprodefsum  25251  iprodefisumlem  25270  iprodefisum  25271  setinds  25348  bdayfo  25543  fobigcup  25654  unisnif  25678  fullfunfnv  25699  axlowdimlem13  25797  fsumcube  26010  ordtoplem  26089  onsucconi  26091  onsucsuccmpi  26097  limsucncmpi  26099  ordcmp  26101  ismblfin  26146  mbfposadd  26153  itg2addnc  26158  ftc1cnnc  26178  ivthALT  26228  locfindis  26275  imaiinfv  26630  eldioph2  26710  elpell1qr2  26825  aomclem4  27022  kelac2  27031  islmodfg  27035  lmhmlnmsplit  27053  pwssplit4  27059  dsmmval2  27070  frlmsslss  27112  pwfi2f1o  27128  islindf4  27176  dgrsub2  27207  mamuvs1  27331  mamuvs2  27332  cytpval  27396  sbeqal2i  27467  stoweidlem17  27633  stoweidlem26  27642  wallispilem4  27684  wallispilem5  27685  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  stirlinglem3  27692  stirlinglem5  27694  stirlinglem8  27697  funresfunco  27856  dfafv2  27863  ndmaovcl  27934  ndmaovcom  27936  el2xptp  27948  resisresindm  27957  rnfdmpr  27964  0mnnnnn0  27971  euhash1  27998  iswrd0i  27999  swrdccatin12lem3c  28023  swrdccatin12lem4  28025  swrdccat3b  28031  frgra3v  28106  frgrancvvdeqlem4  28136  relopabVD  28722  bnj601  28997  cdlemk36  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397
  Copyright terms: Public domain W3C validator