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  prod2id  24150  setinds  24204  bdayfo  24399  fobigcup  24510  unisnif  24534  fullfunfnv  24555  axlowdimlem13  24653  fsumcube  24866  ordtoplem  24945  onsucconi  24947  onsucsuccmpi  24953  limsucncmpi  24955  ordcmp  24957  itg2addnclem  25002  itg2addnc  25004  itgaddnclem2  25009  ftc1cnnc  25024  oprabex2gpop  25138  isunscov  25176  mapex2  25242  2eq3m1  25281  islatalg  25285  isorhom  25313  isoriso  25314  toplat  25392  clfsebsr  25451  com2i  25518  vecval1b  25553  vecval3b  25554  vecax4  25558  vecax5  25559  mulveczer  25581  mulinvsca  25582  muldisc  25583  svli2  25586  osneisi  25633  intopcoaconlem3  25641  intopcoaconc  25643  usptop  25652  islimrs4  25684  bwt2  25694  flfneic  25726  tcnvec  25792  isdivcv2  25795  isder  25809  1alg  25824  algi  25829  dedi  25839  1ded  25840  dmrngcmp  25853  cati  25857  0alg  25858  1cat  25861  dmo  25878  cmpmorp  25881  mrdmcd  25896  homib  25898  cmphmia  25900  cmphmib  25901  iri  25902  ismona  25911  idmon  25919  isepia  25921  idsubidsup  25959  isinob  25964  issrc  25969  propsrc  25970  isntr  25975  islimcat  25978  prismorcsetlemc  26019  prismorcset2  26020  domcatfun  26027  codcatfun  26036  cmp2morpgrp  26065  cmpmorass  26068  morexcmp  26069  pgapspf  26154  bisig0  26164  isibg2  26212  sgplpte21  26234  sgplpte22  26240  nds  26252  isray  26256  isside0  26266  aishp  26274  isibcg  26293  ivthALT  26360  locfindis  26407  imaiinfv  26861  eldioph2  26943  elpell1qr2  27059  aomclem4  27256  kelac2  27265  islmodfg  27269  lmhmlnmsplit  27287  pwssplit4  27293  dsmmval2  27304  frlmsslss  27346  pwfi2f1o  27362  islindf4  27410  dgrsub2  27441  mamuvs1  27565  mamuvs2  27566  cytpval  27630  sbeqal2i  27701  compneOLD  27745  stoweidlem17  27868  stoweidlem26  27877  stoweidlem34  27885  wallispilem4  27919  wallispilem5  27920  wallispi  27921  wallispi2lem1  27922  wallispi2lem2  27923  stirlinglem1  27925  stirlinglem5  27929  stirlinglem8  27932  stirlinglem14  27938  funresfunco  28092  dfafv2  28099  ndmaovcl  28170  ndmaovcom  28172  f1oprg  28185  f1oun2prg  28186  fzo0to42pr  28210  usgraexvlem  28260  nb3graprlem2  28287  nb3grapr  28288  nb3grapr2  28289  nb3gra2nb  28290  0wlk  28342  0trl  28343  wlkntrllem1  28344  wlkntrllem3  28346  wlkntrllem5  28348  0crct  28370  0cycl  28371  constr3trllem3  28397  constr3pthlem1  28400  constr3pthlem3  28402  frgra3v  28425  relopabVD  28992  bnj601  29267  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