Theorem eqcomi 2233

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  eqtr3id  2276  eqtr3di  2277  eqtr4di  2280  eqtr4id  2281  eqeltrri  2303  eleqtrri  2305  eqeltrrid  2317  eleqtrrdi  2323  abid2  2350  abid2f  2398  eqnetrri  2425  neeqtrri  2429  eqsstrri  3257  sseqtrri  3259  eqsstrrid  3271  sseqtrrdi  3273  difdif2ss  3461  inrab2  3477  dfopg  3854  opid  3874  eqbrtrri  4105  breqtrri  4109  breqtrrdi  4124  opwo0id  4334  pwin  4372  limon  4604  tfis  4674  dfdm2  5262  cnvresid  5394  fores  5557  funcoeqres  5602  f1oprg  5616  fvmbr  5661  fnmptfvd  5738  funopdmsn  5818  fmptpr  5830  fsnunres  5840  idref  5879  riotaeqimp  5978  riotaprop  5979  fo1st  6301  fo2nd  6302  fnmpoovd  6359  ixpsnf1o  6881  phplem4  7012  snnen2og  7016  phplem4on  7025  pw1dc0el  7069  ss1o0el1o  7071  sbthlemi5  7124  eldju  7231  casefun  7248  omp1eomlem  7257  exmidfodomrlemim  7375  caucvgsrlembound  7977  ax0id  8061  1p1e2  9223  1e2m1  9225  2p1e3  9240  3p1e4  9242  4p1e5  9243  5p1e6  9244  6p1e7  9245  7p1e8  9246  8p1e9  9247  div4p1lem1div2  9361  0mnnnnn0  9397  zeo  9548  num0u  9584  numsucc  9613  decsucc  9614  1e0p1  9615  nummac  9618  decsubi  9636  decmul1  9637  decmul10add  9642  6p5lem  9643  10m1e9  9669  5t5e25  9676  6t6e36  9681  8t6e48  9692  decbin3  9715  infrenegsupex  9785  ige3m2fz  10241  fseq1p1m1  10286  fz0tp  10314  fz0to4untppr  10316  1fv  10331  fzo0to42pr  10421  fzosplitprm1  10435  fldiv4lem1div2uz2  10521  xnn0nnen  10654  expnegap0  10764  sq4e2t8  10854  3dec  10931  fihashen1  11016  pr0hash2ex  11032  fundm2domnop0  11062  pfxccat3  11261  swrdccat  11262  pfxccatpfx2  11264  swrdccat3blem  11266  swrdccat3b  11267  cats2catd  11296  imi  11406  infxrnegsupex  11769  zsumdc  11890  fsumadd  11912  hashrabrex  11987  ntrivcvgap  12054  fprodmul  12097  fproddivapf  12137  fprodmodd  12147  efsep  12197  3dvds  12370  3dvdsdec  12371  3dvds2dec  12372  flodddiv4  12442  lcmneg  12591  dec2dvds  12929  2exp5  12950  2exp11  12954  ennnfonelem1  12973  nninfdclemp1  13016  ndxid  13051  2strstr1g  13150  srgfcl  13931  isrhm  14116  issubrng  14157  rmodislmod  14309  cnfld0  14529  cnfld1  14530  cnfldplusf  14532  cnfldui  14547  toponrestid  14689  istpsi  14707  distopon  14755  distps  14759  discld  14804  txbas  14926  txdis  14945  txdis1cn  14946  txhmeo  14987  txswaphmeolem  14988  dvmptidcn  15382  dvmptid  15384  sinq34lt0t  15499  loge  15535  2logb9irr  15639  2logb9irrALT  15642  sqrt2cxp2logb9e3  15643  2logb9irrap  15645  lgsdir  15708  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2lgsoddprmlem3d  15783  2sqlem9  15797  2sqlem10  15798  setsvtx  15846  edgiedgbg  15859  edg0iedg0g  15860  isuhgrm  15865  isushgrm  15866  uhgr0  15879  isupgren  15889  isumgren  15899  umgrpredgv  15939  isuspgren  15949  isusgren  15950  ausgrusgrben  15960  usgrf1oedg  15997  uhgr2edg  15998  usgredg3  16006  ushgredgedg  16018  ushgredgedgloop  16020  ex-ceil  16048  ex-gcd  16053  bj-charfundcALT  16130  bdceqir  16165  bj-ssom  16257  trilpolemgt1  16366  redcwlpolemeq1  16381