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

Theorem eqcomi 2393
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 2391 . 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  2410  eqtr3i  2411  eqtr4i  2412  syl5eqr  2435  syl5reqr  2436  syl6eqr  2439  syl6reqr  2440  eqeltrri  2460  eleqtrri  2462  syl5eqelr  2474  syl6eleqr  2480  abid2  2506  abid2f  2550  eqnetrri  2571  neeqtrri  2575  eqsstr3i  3324  sseqtr4i  3326  syl5eqssr  3338  syl6sseqr  3340  difdif2  3543  inrab2  3559  opid  3946  eqbrtrri  4176  breqtrri  4180  syl6breqr  4195  pwin  4430  unizlim  4640  orduniss2  4755  limon  4758  orduninsuc  4765  tfis  4776  dfdm2  5343  cnvresid  5465  fores  5604  funcoeqres  5648  f1oprg  5660  fsnunres  5875  soisores  5988  fo1st  6307  fo2nd  6308  1st2val  6313  2nd2val  6314  cnvf1olem  6385  riotaprop  6511  riotaund  6524  seqomlem1  6645  om0r  6721  ixpsnf1o  7040  sbthlem5  7159  fodomr  7196  phplem4  7227  dif1enOLD  7278  dif1en  7279  fodomfi  7323  mapfien  7588  r1suc  7631  rankval4  7728  dif1card  7827  cardnum  7910  fin1a2lem13  8227  itunisuc  8234  ituniiun  8237  ttukeylem4  8327  alephval2  8382  recmulnq  8776  1lt2nq  8785  ltexnq  8787  mul02lem1  9176  addid1  9180  1p1e2  10028  3m1e2OLD  10031  2p1e3  10037  3p1e4  10038  4p1e5  10039  5p1e6  10040  6p1e7  10041  7p1e8  10042  8p1e9  10043  9p1e10  10044  zeo  10289  num0u  10325  numsucc  10342  1e0p1  10344  nummac  10348  6p5lem  10365  5t5e25  10392  6t6e36  10397  8t6e48  10408  decbin3  10421  1fv  11052  fseq1p1m1  11054  fzo0to42pr  11115  expneg  11318  faclbnd4lem1  11513  bcn2m1  11544  bcn2p1  11545  hash2pr  11616  eqs1  11690  f1oun2prg  11793  s0s1  11798  imi  11891  abs1m  12068  caucvg  12401  sum2id  12431  incexclem  12545  incexc  12546  efsep  12640  pockthi  13204  dec2dvds  13328  1259prm  13384  2503prm  13388  4001prm  13393  homffval  13846  xpchomfval  14205  xpccofval  14208  yonedalem3b  14305  oduposb  14492  oduglb  14495  odulub  14497  psssdm2  14576  letsr  14601  gsumwspan  14720  mulgpropd  14852  odlem1  15102  gexlem1  15142  sylow2a  15182  oppglsm  15205  0frgp  15340  ablfac1eu  15560  prdsmgp  15645  pwsmgp  15653  isrhm  15753  drngui  15770  abvtrivd  15857  rlmval  16193  opsrbaslem  16467  psr1val  16513  ply1plusgfvi  16565  cnfld0  16650  cnfld1  16651  cnfldplusf  16653  xrge0cmn  16665  gzrngunit  16689  zzngim  16758  istpsi  16934  distopon  16986  indislem  16989  indistps2ALT  17003  distps  17004  discld  17078  restcls  17169  restntr  17170  dishaus  17370  discmp  17385  cmpsub  17387  2ndcsep  17445  txbas  17522  txdis  17587  txdis1cn  17590  txkgen  17607  xkopt  17610  xkofvcn  17639  hmphdis  17751  hmphindis  17752  txhmeo  17758  txswaphmeolem  17759  xpstopnlem1  17764  ptcmpfi  17768  tmdgsum  18048  symgtgp  18054  fmucndlem  18244  cuspcvg  18254  imasdsf1olem  18313  nrginvrcn  18600  idnghm  18650  xrsmopn  18716  zcld2  18719  metnrmlem2  18763  dfii3  18786  cncfcn1  18813  cncfmpt2f  18817  cdivcncf  18820  abscncfALT  18823  icopnfhmeo  18841  iccpnfhmeo  18843  xrhmeo  18844  cnrehmeo  18851  lebnumii  18864  pcoass  18922  clmzlmvsca  18994  cncmet  19146  cnflduss  19179  itg2cnlem2  19523  iblcnlem1  19548  itgcnlem  19550  limcdif  19632  cnlimc  19644  dvidlem  19671  dvcnp2  19675  dvcn  19676  dvnres  19686  dvaddbr  19693  dvmulbr  19694  dvcobr  19701  dvcjbr  19704  dvexp  19708  dvrec  19710  dvexp3  19731  dveflem  19732  dvlipcn  19747  lhop1lem  19766  ftc1cn  19796  mpff  19831  deg1fvi  19877  dgrlt  20053  dgradd2  20055  coecj  20065  dvply1  20070  plyremlem  20090  aalioulem2  20119  dvtaylp  20155  taylthlem2  20159  psercn  20211  pserdvlem2  20213  pserdv  20214  abelth  20226  sinq34lt0t  20286  sincos6thpi  20292  efifo  20318  eff1olem  20319  loge  20350  logcn  20407  dvloglem  20408  dvlog  20411  dvlog2  20413  efopnlem2  20417  logtayl  20420  logccv  20423  cxpsqrlem  20462  cxpcn  20498  cxpcn2  20499  cxpcn3  20501  resqrcn  20502  sqrcn  20503  dvatan  20644  birthday  20662  divsqrsumlem  20687  emgt0  20714  ftalem3  20726  basellem5  20736  cht2  20824  cht3  20825  chtublem  20864  logfacbnd3  20876  logexprlim  20878  dchr1cl  20904  dchrinvcl  20906  dchrfi  20908  dchrinv  20914  bclbnd  20933  bposlem6  20942  bposlem8  20944  lgsdir2lem2  20977  lgsdir  20983  2sqlem9  21026  2sqlem10  21027  dchrisum0flblem1  21071  logdivsum  21096  log2sumbnd  21107  ostth2  21200  ostth  21202  ausisusgra  21249  usgraexvlem  21282  nb3graprlem2  21329  nb3grapr  21330  nb3grapr2  21331  nb3gra2nb  21332  cusgraexilem2  21344  0wlk  21411  0trl  21412  wlkntrllem1  21415  wlkntrllem3  21417  wlkntrllem5  21419  constr1trl  21438  constr2trl  21448  0crct  21463  0cycl  21464  constr3trllem3  21489  ex-dif  21581  1p1e2apr1  21610  isgrpoi  21636  grpofo  21637  0ngrp  21649  grpo2grp  21672  isass  21754  ismgm  21758  gidsn  21786  ginvsn  21787  rngosn  21842  rngoueqz  21868  bafval  21933  nvdm  22000  nvtri  22009  nmcnc  22042  cnbn  22221  hvsubcan2i  22416  normlem1  22462  normlem2  22463  bcseqi  22472  normpar2i  22508  hhnv  22517  hhssabloi  22612  hhshsslem1  22617  hhssvs  22622  hhsscms  22629  shscli  22669  ococi  22757  qlax1i  22979  qlaxr1i  22984  hosd1i  23175  nmcexi  23379  pjin1i  23545  hatomistici  23715  addltmulALT  23799  fmptpr  23906  rhmopp  24075  tpr2uni  24109  rmulccn  24120  xrge0iifhmeo  24128  xrge0pluscn  24132  xrge0mulc1cn  24133  xrge0topn  24135  xrge0tmdOLD  24137  qqh0  24169  qqh1  24170  rrhval  24180  rrhcn  24181  rrhre  24185  esumnul  24241  esum0  24242  esumpfinval  24263  esumpfinvalf  24264  esumpcvgval  24266  ballotth  24576  zetacvg  24580  ntrivcvg  25006  prod2id  25035  fproddiv  25066  fprodfac  25077  fprodabs  25078  fprodefsum  25079  setinds  25160  bdayfo  25355  fobigcup  25466  unisnif  25490  fullfunfnv  25511  axlowdimlem13  25609  fsumcube  25822  ordtoplem  25901  onsucconi  25903  onsucsuccmpi  25909  limsucncmpi  25911  ordcmp  25913  itg2addnclem  25959  itg2addnc  25961  itgaddnclem2  25966  ftc1cnnc  25981  ivthALT  26031  locfindis  26078  imaiinfv  26433  eldioph2  26513  elpell1qr2  26628  aomclem4  26825  kelac2  26834  islmodfg  26838  lmhmlnmsplit  26856  pwssplit4  26862  dsmmval2  26873  frlmsslss  26915  pwfi2f1o  26931  islindf4  26979  dgrsub2  27010  mamuvs1  27134  mamuvs2  27135  cytpval  27199  sbeqal2i  27270  stoweidlem17  27436  stoweidlem26  27445  wallispilem4  27487  wallispilem5  27488  wallispi2lem1  27490  wallispi2lem2  27491  stirlinglem1  27493  stirlinglem3  27495  stirlinglem5  27497  stirlinglem8  27500  funresfunco  27660  dfafv2  27667  ndmaovcl  27738  ndmaovcom  27740  frgra3v  27757  frgrancvvdeqlem4  27787  relopabVD  28356  bnj601  28631  cdlemk36  31029
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 2370
This theorem depends on definitions:  df-bi 178  df-cleq 2382
  Copyright terms: Public domain W3C validator