Theorem eqcomi 2235

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 2233	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 145	1 |- B = A

Syntax hints:   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqtr2i  2253  eqtr3i  2254  eqtr4i  2255  eqtr3id  2278  eqtr3di  2279  eqtr4di  2282  eqtr4id  2283  eqeltrri  2305  eleqtrri  2307  eqeltrrid  2319  eleqtrrdi  2325  abid2  2353  abid2f  2401  eqnetrri  2428  neeqtrri  2432  eqsstrri  3261  sseqtrri  3263  eqsstrrid  3275  sseqtrrdi  3277  difdif2ss  3466  inrab2  3482  dfopg  3865  opid  3885  eqbrtrri  4116  breqtrri  4120  breqtrrdi  4135  opwo0id  4347  pwin  4385  limon  4617  tfis  4687  dfdm2  5278  cnvresid  5411  fores  5578  funcoeqres  5623  f1oprg  5638  fvmbr  5683  fnmptfvd  5760  funopdmsn  5842  fmptpr  5854  fsnunres  5864  idref  5907  riotaeqimp  6006  riotaprop  6007  fo1st  6329  fo2nd  6330  fnmpoovd  6389  ixpsnf1o  6948  phplem4  7084  snnen2og  7088  phplem4on  7097  pw1dc0el  7146  ss1o0el1o  7148  sbthlemi5  7203  eldju  7310  casefun  7327  omp1eomlem  7336  exmidfodomrlemim  7455  caucvgsrlembound  8057  ax0id  8141  1p1e2  9302  1e2m1  9304  2p1e3  9319  3p1e4  9321  4p1e5  9322  5p1e6  9323  6p1e7  9324  7p1e8  9325  8p1e9  9326  div4p1lem1div2  9440  0mnnnnn0  9476  zeo  9629  num0u  9665  numsucc  9694  decsucc  9695  1e0p1  9696  nummac  9699  decsubi  9717  decmul1  9718  decmul10add  9723  6p5lem  9724  10m1e9  9750  5t5e25  9757  6t6e36  9762  8t6e48  9773  decbin3  9796  infrenegsupex  9872  ige3m2fz  10329  fseq1p1m1  10374  fz0tp  10402  fz0to4untppr  10404  1fv  10419  fzo0to42pr  10511  fzosplitpr  10525  fzosplitprm1  10526  fldiv4lem1div2uz2  10612  xnn0nnen  10745  expnegap0  10855  sq4e2t8  10945  3dec  11022  fihashen1  11107  pr0hash2ex  11125  fundm2domnop0  11158  pfxccat3  11364  swrdccat  11365  pfxccatpfx2  11367  swrdccat3blem  11369  swrdccat3b  11370  cats2catd  11399  imi  11523  infxrnegsupex  11886  zsumdc  12008  fsumadd  12030  hashrabrex  12105  ntrivcvgap  12172  fprodmul  12215  fproddivapf  12255  fprodmodd  12265  efsep  12315  3dvds  12488  3dvdsdec  12489  3dvds2dec  12490  flodddiv4  12560  lcmneg  12709  dec2dvds  13047  2exp5  13068  2exp11  13072  ennnfonelem1  13091  nninfdclemp1  13134  ndxid  13169  2strstr1g  13268  srgfcl  14050  isrhm  14236  issubrng  14277  rmodislmod  14430  cnfld0  14650  cnfld1  14651  cnfldplusf  14653  cnfldui  14668  toponrestid  14815  istpsi  14833  distopon  14881  distps  14885  discld  14930  txbas  15052  txdis  15071  txdis1cn  15072  txhmeo  15113  txswaphmeolem  15114  dvmptidcn  15508  dvmptid  15510  sinq34lt0t  15625  loge  15661  2logb9irr  15765  2logb9irrALT  15768  sqrt2cxp2logb9e3  15769  2logb9irrap  15771  lgsdir  15837  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2lgsoddprmlem3d  15912  2sqlem9  15926  2sqlem10  15927  setsvtx  15975  edgiedgbg  15989  edg0iedg0g  15990  isuhgrm  15995  isushgrm  15996  uhgr0  16009  isupgren  16019  isumgren  16029  umgrpredgv  16071  isuspgren  16081  isusgren  16082  ausgrusgrben  16092  usgrf1oedg  16129  uhgr2edg  16130  usgredg3  16138  ushgredgedg  16150  ushgredgedgloop  16152  usgr0  16163  egrsubgr  16187  0grsubgr  16188  vtxdfifiun  16221  edginwlkd  16279  wlk1walkdom  16283  clwwlknon2x  16359  clwwlknonex2lem1  16361  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  ex-ceil  16423  ex-gcd  16428  bj-charfundcALT  16508  bdceqir  16543  bj-ssom  16635  trilpolemgt1  16754  redcwlpolemeq1  16770