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

Theorem eqcomi 2287
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 2285 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 199 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  eqtr2i  2304  eqtr3i  2305  eqtr4i  2306  syl5eqr  2329  syl5reqr  2330  syl6eqr  2333  syl6reqr  2334  eqeltrri  2354  eleqtrri  2356  syl5eqelr  2368  syl6eleqr  2374  abid2  2400  abid2f  2444  eqnetrri  2465  neeqtrri  2469  eqsstr3i  3209  sseqtr4i  3211  syl5eqssr  3223  syl6sseqr  3225  inrab2  3441  opid  3814  eqbrtrri  4044  breqtrri  4048  syl6breqr  4063  pwin  4297  unizlim  4509  orduniss2  4624  limon  4627  orduninsuc  4634  tfis  4645  dfdm2  5204  cnvresid  5322  fores  5460  funcoeqres  5504  fsnunres  5721  soisores  5824  fo1st  6139  fo2nd  6140  1st2val  6145  2nd2val  6146  cnvf1olem  6216  riotaprop  6328  riotaund  6341  seqomlem1  6462  om0r  6538  ixpsnf1o  6856  sbthlem5  6975  fodomr  7012  phplem4  7043  dif1enOLD  7090  dif1en  7091  fodomfi  7135  mapfien  7399  r1suc  7442  rankval4  7539  dif1card  7638  cardnum  7721  fin1a2lem13  8038  itunisuc  8045  ituniiun  8048  ttukeylem4  8139  alephval2  8194  recmulnq  8588  1lt2nq  8597  ltexnq  8599  mul02lem1  8988  addid1  8992  1p1e2  9840  2p1e3  9847  3p1e4  9848  4p1e5  9849  5p1e6  9850  6p1e7  9851  7p1e8  9852  8p1e9  9853  9p1e10  9854  zeo  10097  num0u  10133  numsucc  10150  1e0p1  10152  nummac  10156  6p5lem  10173  5t5e25  10200  6t6e36  10205  8t6e48  10216  decbin3  10229  fseq1p1m1  10857  expneg  11111  faclbnd4lem1  11306  eqs1  11447  s0s1  11549  imi  11642  abs1m  11819  caucvg  12151  sum2id  12181  incexclem  12295  incexc  12296  efsep  12390  pockthi  12954  dec2dvds  13078  1259prm  13134  2503prm  13138  4001prm  13143  homffval  13594  xpchomfval  13953  xpccofval  13956  yonedalem3b  14053  oduposb  14240  oduglb  14243  odulub  14245  psssdm2  14324  letsr  14349  gsumwspan  14468  mulgpropd  14600  odlem1  14850  gexlem1  14890  sylow2a  14930  oppglsm  14953  0frgp  15088  ablfac1eu  15308  prdsmgp  15393  pwsmgp  15401  isrhm  15501  drngui  15518  abvtrivd  15605  rlmval  15945  opsrbaslem  16219  psr1val  16265  ply1plusgfvi  16320  cnfld0  16398  cnfld1  16399  cnfldplusf  16401  xrge0cmn  16413  gzrngunit  16437  zzngim  16506  istpsi  16682  distopon  16734  indislem  16737  indistps2ALT  16751  distps  16752  discld  16826  restcls  16911  restntr  16912  dishaus  17110  discmp  17125  cmpsub  17127  2ndcsep  17185  txbas  17262  txdis  17326  txdis1cn  17329  txkgen  17346  xkopt  17349  xkofvcn  17378  hmphdis  17487  hmphindis  17488  txhmeo  17494  txswaphmeolem  17495  xpstopnlem1  17500  ptcmpfi  17504  tmdgsum  17778  symgtgp  17784  imasdsf1olem  17937  nrginvrcn  18202  idnghm  18252  xrsmopn  18318  zcld2  18321  metnrmlem2  18364  dfii3  18387  cncfcn1  18414  cncfmpt2f  18418  cdivcncf  18420  abscncfALT  18423  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  cnrehmeo  18451  lebnumii  18464  pcoass  18522  clmzlmvsca  18594  cncmet  18744  itg2cnlem2  19117  iblcnlem1  19142  itgcnlem  19144  limcdif  19226  cnlimc  19238  dvidlem  19265  dvcnp2  19269  dvcn  19270  dvnres  19280  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvexp  19302  dvrec  19304  dvexp3  19325  dveflem  19326  dvlipcn  19341  lhop1lem  19360  ftc1cn  19390  mpff  19425  deg1fvi  19471  dgrlt  19647  dgradd2  19649  coecj  19659  dvply1  19664  plyremlem  19684  aalioulem2  19713  dvtaylp  19749  taylthlem2  19753  psercn  19802  pserdvlem2  19804  pserdv  19805  abelth  19817  sinq34lt0t  19877  sincos6thpi  19883  efifo  19909  eff1olem  19910  loge  19940  logcn  19994  dvloglem  19995  dvlog  19998  dvlog2  20000  efopnlem2  20004  logtayl  20007  logccv  20010  cxpsqrlem  20049  cxpcn  20085  cxpcn2  20086  cxpcn3  20088  resqrcn  20089  sqrcn  20090  dvatan  20231  birthday  20249  divsqrsumlem  20274  emgt0  20300  ftalem3  20312  basellem5  20322  cht2  20410  cht3  20411  chtublem  20450  chtub  20451  logfacbnd3  20462  logexprlim  20464  dchr1cl  20490  dchrinvcl  20492  dchrfi  20494  dchrinv  20500  bclbnd  20519  bposlem6  20528  bposlem8  20530  lgsdir2lem2  20563  lgsdir  20569  2sqlem9  20612  2sqlem10  20613  dchrisum0flblem1  20657  logdivsum  20682  log2sumbnd  20693  ostth2  20786  ostth  20788  ex-dif  20810  1p1e2apr1  20839  isgrpoi  20865  grpofo  20866  0ngrp  20878  grpo2grp  20901  isass  20983  ismgm  20987  gidsn  21015  ginvsn  21016  rngosn  21071  rngoueqz  21097  bafval  21160  nvdm  21227  nvtri  21236  nmcnc  21269  cnbn  21448  hvsubcan2i  21643  normlem1  21689  normlem2  21690  bcseqi  21699  normpar2i  21735  hhnv  21744  hhssabloi  21839  hhshsslem1  21844  hhssvs  21849  hhsscms  21856  shscli  21896  ococi  21984  qlax1i  22206  qlaxr1i  22211  hosd1i  22402  nmcexi  22606  pjin1i  22772  hatomistici  22942  addltmulALT  23026  ballotth  23096  fmptpr  23214  tpr2uni  23288  rmulccn  23301  xrge0iifhmeo  23318  xrge0pluscn  23322  xrge0mulc1cn  23323  xrge0topn  23325  xrge0tmdALT  23327  esumnul  23427  esum0  23428  esumpfinval  23443  esumpfinvalf  23444  esumpcvgval  23446  zetacvg  23689  setinds  24134  bdayfo  24329  fobigcup  24440  unisnif  24464  fullfunfnv  24484  axlowdimlem13  24582  fsumcube  24795  ordtoplem  24874  onsucconi  24876  onsucsuccmpi  24882  limsucncmpi  24884  ordcmp  24886  oprabex2gpop  25036  isunscov  25074  mapex2  25140  2eq3m1  25179  islatalg  25183  isorhom  25211  isoriso  25212  toplat  25290  clfsebsr  25349  com2i  25416  vecval1b  25451  vecval3b  25452  vecax4  25456  vecax5  25457  mulveczer  25479  mulinvsca  25480  muldisc  25481  svli2  25484  osneisi  25531  intopcoaconlem3  25539  intopcoaconc  25541  usptop  25550  islimrs4  25582  bwt2  25592  flfneic  25624  tcnvec  25690  isdivcv2  25693  isder  25707  1alg  25722  algi  25727  dedi  25737  1ded  25738  dmrngcmp  25751  cati  25755  0alg  25756  1cat  25759  dmo  25776  cmpmorp  25779  mrdmcd  25794  homib  25796  cmphmia  25798  cmphmib  25799  iri  25800  ismona  25809  idmon  25817  isepia  25819  idsubidsup  25857  isinob  25862  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  prismorcsetlemc  25917  prismorcset2  25918  domcatfun  25925  codcatfun  25934  cmp2morpgrp  25963  cmpmorass  25966  morexcmp  25967  pgapspf  26052  bisig0  26062  isibg2  26110  sgplpte21  26132  sgplpte22  26138  nds  26150  isray  26154  isside0  26164  aishp  26172  isibcg  26191  ivthALT  26258  locfindis  26305  imaiinfv  26759  eldioph2  26841  elpell1qr2  26957  aomclem4  27154  kelac2  27163  islmodfg  27167  lmhmlnmsplit  27185  pwssplit4  27191  dsmmval2  27202  frlmsslss  27244  pwfi2f1o  27260  islindf4  27308  dgrsub2  27339  mamuvs1  27463  mamuvs2  27464  cytpval  27528  sbeqal2i  27599  compneOLD  27643  stoweidlem17  27766  stoweidlem26  27775  stoweidlem34  27783  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  stirlinglem5  27827  stirlinglem8  27830  stirlinglem14  27836  funresfunco  27988  dfafv2  27995  ndmaovcl  28063  ndmaovcom  28065  f1oprg  28075  f1oun2prg  28076  usgraexvlem  28127  frgra3v  28180  relopabVD  28677  bnj601  28952  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator