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

Theorem eqcomi 2416
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 2414 . 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  2433  eqtr3i  2434  eqtr4i  2435  syl5eqr  2458  syl5reqr  2459  syl6eqr  2462  syl6reqr  2463  eqeltrri  2483  eleqtrri  2485  syl5eqelr  2497  syl6eleqr  2503  abid2  2529  abid2f  2573  eqnetrri  2594  neeqtrri  2598  eqsstr3i  3347  sseqtr4i  3349  syl5eqssr  3361  syl6sseqr  3363  difdif2  3566  inrab2  3582  opid  3970  eqbrtrri  4201  breqtrri  4205  syl6breqr  4220  pwin  4455  unizlim  4665  orduniss2  4780  limon  4783  orduninsuc  4790  tfis  4801  dfdm2  5368  cnvresid  5490  fores  5629  funcoeqres  5673  f1oprg  5685  fsnunres  5901  soisores  6014  fo1st  6333  fo2nd  6334  1st2val  6339  2nd2val  6340  cnvf1olem  6411  riotaprop  6540  riotaund  6553  seqomlem1  6674  om0r  6750  ixpsnf1o  7069  sbthlem5  7188  fodomr  7225  phplem4  7256  dif1enOLD  7307  dif1en  7308  fodomfi  7352  mapfien  7617  r1suc  7660  rankval4  7757  dif1card  7856  cardnum  7939  fin1a2lem13  8256  itunisuc  8263  ituniiun  8266  ttukeylem4  8356  alephval2  8411  recmulnq  8805  1lt2nq  8814  ltexnq  8816  mul02lem1  9206  addid1  9210  1p1e2  10058  3m1e2OLD  10061  2p1e3  10067  3p1e4  10068  4p1e5  10069  5p1e6  10070  6p1e7  10071  7p1e8  10072  8p1e9  10073  9p1e10  10074  zeo  10319  num0u  10355  numsucc  10372  1e0p1  10374  nummac  10378  6p5lem  10395  5t5e25  10422  6t6e36  10427  8t6e48  10438  decbin3  10451  fz0tp  11067  1fv  11083  fseq1p1m1  11085  fzo0to42pr  11149  expneg  11352  faclbnd4lem1  11547  bcn2m1  11578  bcn2p1  11579  hash2pr  11650  eqs1  11724  f1oun2prg  11827  s0s1  11832  imi  11925  abs1m  12102  caucvg  12435  sum2id  12465  incexclem  12579  incexc  12580  efsep  12674  pockthi  13238  dec2dvds  13362  1259prm  13418  2503prm  13422  4001prm  13427  homffval  13880  xpchomfval  14239  xpccofval  14242  yonedalem3b  14339  oduposb  14526  oduglb  14529  odulub  14531  psssdm2  14610  letsr  14635  gsumwspan  14754  mulgpropd  14886  odlem1  15136  gexlem1  15176  sylow2a  15216  oppglsm  15239  0frgp  15374  ablfac1eu  15594  prdsmgp  15679  pwsmgp  15687  isrhm  15787  drngui  15804  abvtrivd  15891  rlmval  16227  opsrbaslem  16501  psr1val  16547  ply1plusgfvi  16599  cnfld0  16688  cnfld1  16689  cnfldplusf  16691  xrge0cmn  16703  gzrngunit  16727  zzngim  16796  istpsi  16972  distopon  17024  indislem  17027  indistps2ALT  17041  distps  17042  discld  17116  restcls  17207  restntr  17208  dishaus  17408  discmp  17423  cmpsub  17425  2ndcsep  17483  txbas  17560  txdis  17625  txdis1cn  17628  txkgen  17645  xkopt  17648  xkofvcn  17677  hmphdis  17789  hmphindis  17790  txhmeo  17796  txswaphmeolem  17797  xpstopnlem1  17802  ptcmpfi  17806  tmdgsum  18086  symgtgp  18092  fmucndlem  18282  cuspcvg  18292  imasdsf1olem  18364  nrginvrcn  18688  idnghm  18738  xrsmopn  18804  zcld2  18807  metnrmlem2  18851  dfii3  18874  cncfcn1  18901  cncfmpt2f  18905  cdivcncf  18908  abscncfALT  18911  icopnfhmeo  18929  iccpnfhmeo  18931  xrhmeo  18932  cnrehmeo  18939  lebnumii  18952  pcoass  19010  clmzlmvsca  19082  cncmet  19236  cnflduss  19271  itg2cnlem2  19615  iblcnlem1  19640  itgcnlem  19642  limcdif  19724  cnlimc  19736  dvidlem  19763  dvcnp2  19767  dvcn  19768  dvnres  19778  dvaddbr  19785  dvmulbr  19786  dvcobr  19793  dvcjbr  19796  dvexp  19800  dvrec  19802  dvexp3  19823  dveflem  19824  dvlipcn  19839  lhop1lem  19858  ftc1cn  19888  mpff  19923  deg1fvi  19969  dgrlt  20145  dgradd2  20147  coecj  20157  dvply1  20162  plyremlem  20182  aalioulem2  20211  dvtaylp  20247  taylthlem2  20251  psercn  20303  pserdvlem2  20305  pserdv  20306  abelth  20318  sinq34lt0t  20378  sincos6thpi  20384  efifo  20410  eff1olem  20411  loge  20442  logcn  20499  dvloglem  20500  dvlog  20503  dvlog2  20505  efopnlem2  20509  logtayl  20512  logccv  20515  cxpsqrlem  20554  cxpcn  20590  cxpcn2  20591  cxpcn3  20593  resqrcn  20594  sqrcn  20595  dvatan  20736  birthday  20754  divsqrsumlem  20779  emgt0  20806  ftalem3  20818  basellem5  20828  cht2  20916  cht3  20917  chtublem  20956  logfacbnd3  20968  logexprlim  20970  dchr1cl  20996  dchrinvcl  20998  dchrfi  21000  dchrinv  21006  bclbnd  21025  bposlem6  21034  bposlem8  21036  lgsdir2lem2  21069  lgsdir  21075  2sqlem9  21118  2sqlem10  21119  dchrisum0flblem1  21163  logdivsum  21188  log2sumbnd  21199  ostth2  21292  ostth  21294  ausisusgra  21341  usgraexvlem  21375  nb3graprlem2  21422  nb3grapr  21423  nb3grapr2  21424  nb3gra2nb  21425  cusgraexilem2  21437  0wlk  21506  0trl  21507  2trllemE  21514  wlkntrllem1  21520  wlkntrllem3  21522  constr1trl  21549  0crct  21574  0cycl  21575  constr3trllem3  21600  ex-dif  21692  1p1e2apr1  21721  isgrpoi  21747  grpofo  21748  0ngrp  21760  grpo2grp  21783  isass  21865  ismgm  21869  gidsn  21897  ginvsn  21898  rngosn  21953  rngoueqz  21979  bafval  22044  nvdm  22111  nvtri  22120  nmcnc  22153  cnbn  22332  hvsubcan2i  22527  normlem1  22573  normlem2  22574  bcseqi  22583  normpar2i  22619  hhnv  22628  hhssabloi  22723  hhshsslem1  22728  hhssvs  22733  hhsscms  22740  shscli  22780  ococi  22868  qlax1i  23090  qlaxr1i  23095  hosd1i  23286  nmcexi  23490  pjin1i  23656  hatomistici  23826  addltmulALT  23910  fmptpr  24023  rhmopp  24218  tpr2uni  24264  rmulccn  24275  xrge0iifhmeo  24283  xrge0pluscn  24287  xrge0mulc1cn  24288  xrge0topn  24290  xrge0tmdOLD  24292  rezh  24316  qqh0  24329  qqh1  24330  rrhval  24340  rrhcn  24341  esumnul  24404  esum0  24405  esumpfinval  24426  esumpfinvalf  24427  esumpcvgval  24429  sitmval  24622  sitmcl  24624  ballotth  24756  zetacvg  24760  ntrivcvg  25186  prod2id  25215  fproddiv  25246  fprodfac  25257  fprodabs  25258  fprodefsum  25259  iprodefisumlem  25278  iprodefisum  25279  setinds  25356  bdayfo  25551  fobigcup  25662  unisnif  25686  fullfunfnv  25707  axlowdimlem13  25805  fsumcube  26018  ordtoplem  26097  onsucconi  26099  onsucsuccmpi  26105  limsucncmpi  26107  ordcmp  26109  ismblfin  26154  mbfposadd  26161  itg2addnc  26166  ftc1cnnc  26186  ivthALT  26236  locfindis  26283  imaiinfv  26638  eldioph2  26718  elpell1qr2  26833  aomclem4  27030  kelac2  27039  islmodfg  27043  lmhmlnmsplit  27061  pwssplit4  27067  dsmmval2  27078  frlmsslss  27120  pwfi2f1o  27136  islindf4  27184  dgrsub2  27215  mamuvs1  27339  mamuvs2  27340  cytpval  27404  sbeqal2i  27475  stoweidlem17  27641  stoweidlem26  27650  wallispilem4  27692  wallispilem5  27693  wallispi2lem1  27695  wallispi2lem2  27696  stirlinglem1  27698  stirlinglem3  27700  stirlinglem5  27702  stirlinglem8  27705  funresfunco  27864  dfafv2  27871  ndmaovcl  27942  ndmaovcom  27944  el2xptp  27956  resisresindm  27965  rnfdmpr  27972  0mnnnnn0  27979  euhash1  28006  iswrd0i  28007  swrdccatin12lem3c  28031  swrdccatin12lem4  28033  swrdccat3b  28039  frgra3v  28114  frgrancvvdeqlem4  28144  relopabVD  28731  bnj601  29009  cdlemk36  31407
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 2393
This theorem depends on definitions:  df-bi 178  df-cleq 2405
  Copyright terms: Public domain W3C validator