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

Theorem eqcomi 2440
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 2438 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2mpbi 200 1  |-  B  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  eqtr2i  2457  eqtr3i  2458  eqtr4i  2459  syl5eqr  2482  syl5reqr  2483  syl6eqr  2486  syl6reqr  2487  eqeltrri  2507  eleqtrri  2509  syl5eqelr  2521  syl6eleqr  2527  abid2  2553  abid2f  2597  eqnetrri  2620  neeqtrri  2624  eqsstr3i  3379  sseqtr4i  3381  syl5eqssr  3393  syl6sseqr  3395  difdif2  3598  inrab2  3614  opid  4002  eqbrtrri  4233  breqtrri  4237  syl6breqr  4252  pwin  4487  unizlim  4698  orduniss2  4813  limon  4816  orduninsuc  4823  tfis  4834  dfdm2  5401  cnvresid  5523  fores  5662  funcoeqres  5706  f1oprg  5718  fsnunres  5934  soisores  6047  fo1st  6366  fo2nd  6367  1st2val  6372  2nd2val  6373  cnvf1olem  6444  riotaprop  6573  riotaund  6586  seqomlem1  6707  om0r  6783  ixpsnf1o  7102  sbthlem5  7221  fodomr  7258  phplem4  7289  dif1enOLD  7340  dif1en  7341  fodomfi  7385  infssuni  7397  mapfien  7653  r1suc  7696  rankval4  7793  dif1card  7892  cardnum  7975  fin1a2lem13  8292  itunisuc  8299  ituniiun  8302  ttukeylem4  8392  alephval2  8447  recmulnq  8841  1lt2nq  8850  ltexnq  8852  mul02lem1  9242  addid1  9246  1p1e2  10094  3m1e2OLD  10097  2p1e3  10103  3p1e4  10104  4p1e5  10105  5p1e6  10106  6p1e7  10107  7p1e8  10108  8p1e9  10109  9p1e10  10110  zeo  10355  num0u  10391  numsucc  10408  1e0p1  10410  nummac  10414  6p5lem  10431  5t5e25  10458  6t6e36  10463  8t6e48  10474  decbin3  10487  fz0tp  11103  1fv  11120  fseq1p1m1  11122  fzo0to42pr  11186  expneg  11389  faclbnd4lem1  11584  bcn2m1  11615  bcn2p1  11616  hash2pr  11687  eqs1  11761  f1oun2prg  11864  s0s1  11869  imi  11962  abs1m  12139  caucvg  12472  sum2id  12502  incexclem  12616  incexc  12617  efsep  12711  pockthi  13275  dec2dvds  13399  1259prm  13455  2503prm  13459  4001prm  13464  homffval  13917  xpchomfval  14276  xpccofval  14279  yonedalem3b  14376  oduposb  14563  oduglb  14566  odulub  14568  psssdm2  14647  letsr  14672  gsumwspan  14791  mulgpropd  14923  odlem1  15173  gexlem1  15213  sylow2a  15253  oppglsm  15276  0frgp  15411  ablfac1eu  15631  prdsmgp  15716  pwsmgp  15724  isrhm  15824  drngui  15841  abvtrivd  15928  rlmval  16264  opsrbaslem  16538  psr1val  16584  ply1plusgfvi  16636  cnfld0  16725  cnfld1  16726  cnfldplusf  16728  xrge0cmn  16740  gzrngunit  16764  zzngim  16833  istpsi  17009  distopon  17061  indislem  17064  indistps2ALT  17078  distps  17079  discld  17153  restcls  17245  restntr  17246  dishaus  17446  discmp  17461  cmpsub  17463  bwth  17473  2ndcsep  17522  txbas  17599  txdis  17664  txdis1cn  17667  txkgen  17684  xkopt  17687  xkofvcn  17716  hmphdis  17828  hmphindis  17829  txhmeo  17835  txswaphmeolem  17836  xpstopnlem1  17841  ptcmpfi  17845  tmdgsum  18125  symgtgp  18131  fmucndlem  18321  cuspcvg  18331  imasdsf1olem  18403  nrginvrcn  18727  idnghm  18777  xrsmopn  18843  zcld2  18846  metnrmlem2  18890  dfii3  18913  cncfcn1  18940  cncfmpt2f  18944  cdivcncf  18947  abscncfALT  18950  icopnfhmeo  18968  iccpnfhmeo  18970  xrhmeo  18971  cnrehmeo  18978  lebnumii  18991  pcoass  19049  clmzlmvsca  19121  cncmet  19275  cnflduss  19310  itg2cnlem2  19654  iblcnlem1  19679  itgcnlem  19681  limcdif  19763  cnlimc  19775  dvidlem  19802  dvcnp2  19806  dvcn  19807  dvnres  19817  dvaddbr  19824  dvmulbr  19825  dvcobr  19832  dvcjbr  19835  dvexp  19839  dvrec  19841  dvexp3  19862  dveflem  19863  dvlipcn  19878  lhop1lem  19897  ftc1cn  19927  mpff  19962  deg1fvi  20008  dgrlt  20184  dgradd2  20186  coecj  20196  dvply1  20201  plyremlem  20221  aalioulem2  20250  dvtaylp  20286  taylthlem2  20290  psercn  20342  pserdvlem2  20344  pserdv  20345  abelth  20357  sinq34lt0t  20417  sincos6thpi  20423  efifo  20449  eff1olem  20450  loge  20481  logcn  20538  dvloglem  20539  dvlog  20542  dvlog2  20544  efopnlem2  20548  logtayl  20551  logccv  20554  cxpsqrlem  20593  cxpcn  20629  cxpcn2  20630  cxpcn3  20632  resqrcn  20633  sqrcn  20634  dvatan  20775  birthday  20793  divsqrsumlem  20818  emgt0  20845  ftalem3  20857  basellem5  20867  cht2  20955  cht3  20956  chtublem  20995  logfacbnd3  21007  logexprlim  21009  dchr1cl  21035  dchrinvcl  21037  dchrfi  21039  dchrinv  21045  bclbnd  21064  bposlem6  21073  bposlem8  21075  lgsdir2lem2  21108  lgsdir  21114  2sqlem9  21157  2sqlem10  21158  dchrisum0flblem1  21202  logdivsum  21227  log2sumbnd  21238  ostth2  21331  ostth  21333  ausisusgra  21380  usgraexvlem  21414  nb3graprlem2  21461  nb3grapr  21462  nb3grapr2  21463  nb3gra2nb  21464  cusgraexilem2  21476  0wlk  21545  0trl  21546  2trllemE  21553  wlkntrllem1  21559  wlkntrllem3  21561  constr1trl  21588  0crct  21613  0cycl  21614  constr3trllem3  21639  ex-dif  21731  1p1e2apr1  21760  isgrpoi  21786  grpofo  21787  0ngrp  21799  grpo2grp  21822  isass  21904  ismgm  21908  gidsn  21936  ginvsn  21937  rngosn  21992  rngoueqz  22018  bafval  22083  nvdm  22150  nvtri  22159  nmcnc  22192  cnbn  22371  hvsubcan2i  22566  normlem1  22612  normlem2  22613  bcseqi  22622  normpar2i  22658  hhnv  22667  hhssabloi  22762  hhshsslem1  22767  hhssvs  22772  hhsscms  22779  shscli  22819  ococi  22907  qlax1i  23129  qlaxr1i  23134  hosd1i  23325  nmcexi  23529  pjin1i  23695  hatomistici  23865  addltmulALT  23949  fmptpr  24062  rhmopp  24257  tpr2uni  24303  rmulccn  24314  xrge0iifhmeo  24322  xrge0pluscn  24326  xrge0mulc1cn  24327  xrge0topn  24329  xrge0tmdOLD  24331  rezh  24355  qqh0  24368  qqh1  24369  rrhval  24379  rrhcn  24380  esumnul  24443  esum0  24444  esumpfinval  24465  esumpfinvalf  24466  esumpcvgval  24468  sitmval  24661  sitmcl  24663  ballotth  24795  zetacvg  24799  ntrivcvg  25225  prod2id  25254  fproddiv  25285  fprodfac  25296  fprodabs  25297  fprodefsum  25298  iprodefisumlem  25317  iprodefisum  25318  setinds  25405  tfrALTlem  25557  bdayfo  25630  fobigcup  25745  unisnif  25770  fullfunfnv  25791  axlowdimlem13  25893  fsumcube  26106  ordtoplem  26185  onsucconi  26187  onsucsuccmpi  26193  limsucncmpi  26195  ordcmp  26197  ismblfin  26247  mbfposadd  26254  itg2addnc  26259  ftc1cnnc  26279  ivthALT  26338  locfindis  26385  imaiinfv  26740  eldioph2  26820  elpell1qr2  26935  aomclem4  27132  kelac2  27140  islmodfg  27144  lmhmlnmsplit  27162  pwssplit4  27168  dsmmval2  27179  frlmsslss  27221  pwfi2f1o  27237  islindf4  27285  dgrsub2  27316  mamuvs1  27440  mamuvs2  27441  cytpval  27505  sbeqal2i  27576  stoweidlem17  27742  stoweidlem26  27751  wallispilem4  27793  wallispilem5  27794  wallispi2lem1  27796  wallispi2lem2  27797  stirlinglem1  27799  stirlinglem3  27801  stirlinglem5  27803  stirlinglem8  27806  funresfunco  27965  dfafv2  27972  ndmaovcl  28043  ndmaovcom  28045  el2xptp  28060  resisresindm  28074  rnfdmpr  28083  0mnnnnn0  28095  euhash1  28167  iswrd0i  28169  swrdccatin2  28210  swrdccatin12lem3c  28211  swrdccatin12lem4  28213  swrdccatin12  28214  swrdccat3  28215  swrdccat  28216  swrdccat3blem  28218  swrdccat3b  28219  wlkcomp  28301  frgra3v  28392  frgrancvvdeqlem4  28422  relopabVD  29013  bnj601  29291  cdlemk36  31710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429
  Copyright terms: Public domain W3C validator