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 1397

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 1495  ax-gen 1497  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  2352  abid2f  2400  eqnetrri  2427  neeqtrri  2431  eqsstrri  3260  sseqtrri  3262  eqsstrrid  3274  sseqtrrdi  3276  difdif2ss  3464  inrab2  3480  dfopg  3860  opid  3880  eqbrtrri  4111  breqtrri  4115  breqtrrdi  4130  opwo0id  4341  pwin  4379  limon  4611  tfis  4681  dfdm2  5271  cnvresid  5404  fores  5569  funcoeqres  5614  f1oprg  5629  fvmbr  5674  fnmptfvd  5751  funopdmsn  5834  fmptpr  5846  fsnunres  5856  idref  5897  riotaeqimp  5996  riotaprop  5997  fo1st  6320  fo2nd  6321  fnmpoovd  6380  ixpsnf1o  6905  phplem4  7041  snnen2og  7045  phplem4on  7054  pw1dc0el  7103  ss1o0el1o  7105  sbthlemi5  7160  eldju  7267  casefun  7284  omp1eomlem  7293  exmidfodomrlemim  7412  caucvgsrlembound  8014  ax0id  8098  1p1e2  9260  1e2m1  9262  2p1e3  9277  3p1e4  9279  4p1e5  9280  5p1e6  9281  6p1e7  9282  7p1e8  9283  8p1e9  9284  div4p1lem1div2  9398  0mnnnnn0  9434  zeo  9585  num0u  9621  numsucc  9650  decsucc  9651  1e0p1  9652  nummac  9655  decsubi  9673  decmul1  9674  decmul10add  9679  6p5lem  9680  10m1e9  9706  5t5e25  9713  6t6e36  9718  8t6e48  9729  decbin3  9752  infrenegsupex  9828  ige3m2fz  10284  fseq1p1m1  10329  fz0tp  10357  fz0to4untppr  10359  1fv  10374  fzo0to42pr  10466  fzosplitpr  10480  fzosplitprm1  10481  fldiv4lem1div2uz2  10567  xnn0nnen  10700  expnegap0  10810  sq4e2t8  10900  3dec  10977  fihashen1  11062  pr0hash2ex  11080  fundm2domnop0  11113  pfxccat3  11319  swrdccat  11320  pfxccatpfx2  11322  swrdccat3blem  11324  swrdccat3b  11325  cats2catd  11354  imi  11478  infxrnegsupex  11841  zsumdc  11963  fsumadd  11985  hashrabrex  12060  ntrivcvgap  12127  fprodmul  12170  fproddivapf  12210  fprodmodd  12220  efsep  12270  3dvds  12443  3dvdsdec  12444  3dvds2dec  12445  flodddiv4  12515  lcmneg  12664  dec2dvds  13002  2exp5  13023  2exp11  13027  ennnfonelem1  13046  nninfdclemp1  13089  ndxid  13124  2strstr1g  13223  srgfcl  14005  isrhm  14191  issubrng  14232  rmodislmod  14384  cnfld0  14604  cnfld1  14605  cnfldplusf  14607  cnfldui  14622  toponrestid  14764  istpsi  14782  distopon  14830  distps  14834  discld  14879  txbas  15001  txdis  15020  txdis1cn  15021  txhmeo  15062  txswaphmeolem  15063  dvmptidcn  15457  dvmptid  15459  sinq34lt0t  15574  loge  15610  2logb9irr  15714  2logb9irrALT  15717  sqrt2cxp2logb9e3  15718  2logb9irrap  15720  lgsdir  15783  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3d1  15848  2lgsoddprmlem3d  15858  2sqlem9  15872  2sqlem10  15873  setsvtx  15921  edgiedgbg  15935  edg0iedg0g  15936  isuhgrm  15941  isushgrm  15942  uhgr0  15955  isupgren  15965  isumgren  15975  umgrpredgv  16017  isuspgren  16027  isusgren  16028  ausgrusgrben  16038  usgrf1oedg  16075  uhgr2edg  16076  usgredg3  16084  ushgredgedg  16096  ushgredgedgloop  16098  usgr0  16109  egrsubgr  16133  0grsubgr  16134  vtxdfifiun  16167  edginwlkd  16225  wlk1walkdom  16229  clwwlknon2x  16305  clwwlknonex2lem1  16307  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  ex-ceil  16369  ex-gcd  16374  bj-charfundcALT  16455  bdceqir  16490  bj-ssom  16582  trilpolemgt1  16694  redcwlpolemeq1  16710