Theorem eqcomi 2242

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

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 |- A = B
2		eqcom 2240	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 145	1 |- B = A

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  eqtr3id  2285  eqtr3di  2286  eqtr4di  2289  eqtr4id  2290  eqeltrri  2312  eleqtrri  2314  eqeltrrid  2326  eleqtrrdi  2332  abid2  2361  abid2f  2418  eqnetrri  2445  neeqtrri  2449  eqsstrri  3281  sseqtrri  3283  eqsstrrid  3295  sseqtrrdi  3297  difdif2ss  3488  inrab2  3506  dfopg  3902  opid  3922  eqbrtrri  4154  breqtrri  4158  breqtrrdi  4173  opwo0id  4391  pwin  4429  limon  4662  tfis  4732  dfdm2  5325  cnvresid  5458  fores  5628  funcoeqres  5673  f1oprg  5688  fvmbr  5734  fnmptfvd  5816  funopdmsn  5898  fmptpr  5910  fsnunres  5920  idref  5965  riotaeqimp  6066  riotaprop  6067  fo1st  6395  fo2nd  6396  fnmpoovd  6455  ixpsnf1o  7024  phplem4  7162  snnen2og  7166  phplem4on  7175  pw1dc0el  7224  ss1o0el1o  7226  sbthlemi5  7285  eldju  7414  casefun  7431  omp1eomlem  7440  exmidfodomrlemim  7559  caucvgsrlembound  8167  ax0id  8251  1p1e2  9430  1e2m1  9432  2p1e3  9447  3p1e4  9449  4p1e5  9450  5p1e6  9451  6p1e7  9452  7p1e8  9453  8p1e9  9454  div4p1lem1div2  9570  0mnnnnn0  9606  zeo  9761  num0u  9797  numsucc  9831  decsucc  9832  1e0p1  9833  nummac  9836  decsubi  9854  decmul1  9855  decmul10add  9860  6p5lem  9861  10m1e9  9887  5t5e25  9894  6t6e36  9899  8t6e48  9910  decbin3  9933  infrenegsupex  10009  ige3m2fz  10470  fseq1p1m1  10517  fz0tp  10545  fz0to4untppr  10547  1fv  10562  fzo0to42pr  10654  fzosplitpr  10668  fzosplitprm1  10669  fldiv4lem1div2uz2  10761  xnn0nnen  10894  expnegap0  11004  sq4e2t8  11094  3dec  11173  fihashen1  11259  pr0hash2ex  11277  fundm2domnop0  11321  pfxccat3  11527  swrdccat  11528  pfxccatpfx2  11530  swrdccat3blem  11532  swrdccat3b  11533  cats2catd  11562  imi  11687  infxrnegsupex  12053  zsumdc  12175  fsumadd  12197  hashrabrex  12272  ntrivcvgap  12339  fprodmul  12382  fproddivapf  12422  fprodmodd  12432  efsep  12482  3dvds  12655  3dvdsdec  12656  3dvds2dec  12657  flodddiv4  12727  lcmneg  12876  dec2dvds  13218  2exp5  13240  2exp11  13244  1259prm  13275  ballotfilemth  13338  ennnfonelem1  13355  nninfdclemp1  13398  ndxid  13433  2strstr1g  13534  srgfcl  14383  isrhm  14573  issubrng  14615  rmodislmod  14796  cnfld0  15016  cnfld1  15017  cnfldplusf  15019  cnfldui  15032  isassa  15110  assamulgscmlem2  15150  toponrestid  15264  istpsi  15282  distopon  15330  distps  15334  discld  15379  txbas  15501  txdis  15520  txdis1cn  15521  txhmeo  15562  txswaphmeolem  15563  dvmptidcn  15957  dvmptid  15959  sinq34lt0t  16075  loge  16113  2logb9irr  16224  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  2logb9irrap  16230  birthdaylog2  16245  cht2  16293  cht3  16294  chtublem  16312  bclbnd  16324  bposlem6  16333  bposlem8  16335  lgsdir  16376  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3d1  16441  2lgsoddprmlem3d  16451  2sqlem9  16465  2sqlem10  16466  setsvtx  16514  edgiedgbg  16528  edg0iedg0g  16529  isuhgrm  16534  isushgrm  16535  uhgr0  16548  isupgren  16558  isumgren  16568  umgrpredgv  16610  isuspgren  16620  isusgren  16621  ausgrusgrben  16631  usgrf1oedg  16668  uhgr2edg  16669  usgredg3  16677  ushgredgedg  16689  ushgredgedgloop  16691  usgr0  16702  egrsubgr  16726  0grsubgr  16727  vtxdfifiun  16760  edginwlkd  16818  wlk1walkdom  16822  clwwlknon2x  16898  clwwlknonex2lem1  16900  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  ex-ceil  16962  ex-gcd  16967  bj-charfundcALT  17057  bdceqir  17092  bj-ssom  17184  trilpolemgt1  17312  redcwlpolemeq1  17328