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  10465  fzosplitpr  10479  fzosplitprm1  10480  fldiv4lem1div2uz2  10566  xnn0nnen  10699  expnegap0  10809  sq4e2t8  10899  3dec  10976  fihashen1  11061  pr0hash2ex  11079  fundm2domnop0  11109  pfxccat3  11315  swrdccat  11316  pfxccatpfx2  11318  swrdccat3blem  11320  swrdccat3b  11321  cats2catd  11350  imi  11461  infxrnegsupex  11824  zsumdc  11946  fsumadd  11968  hashrabrex  12043  ntrivcvgap  12110  fprodmul  12153  fproddivapf  12193  fprodmodd  12203  efsep  12253  3dvds  12426  3dvdsdec  12427  3dvds2dec  12428  flodddiv4  12498  lcmneg  12647  dec2dvds  12985  2exp5  13006  2exp11  13010  ennnfonelem1  13029  nninfdclemp1  13072  ndxid  13107  2strstr1g  13206  srgfcl  13988  isrhm  14174  issubrng  14215  rmodislmod  14367  cnfld0  14587  cnfld1  14588  cnfldplusf  14590  cnfldui  14605  toponrestid  14747  istpsi  14765  distopon  14813  distps  14817  discld  14862  txbas  14984  txdis  15003  txdis1cn  15004  txhmeo  15045  txswaphmeolem  15046  dvmptidcn  15440  dvmptid  15442  sinq34lt0t  15557  loge  15593  2logb9irr  15697  2logb9irrALT  15700  sqrt2cxp2logb9e3  15701  2logb9irrap  15703  lgsdir  15766  2lgslem3a  15824  2lgslem3b  15825  2lgslem3c  15826  2lgslem3d  15827  2lgslem3d1  15831  2lgsoddprmlem3d  15841  2sqlem9  15855  2sqlem10  15856  setsvtx  15904  edgiedgbg  15918  edg0iedg0g  15919  isuhgrm  15924  isushgrm  15925  uhgr0  15938  isupgren  15948  isumgren  15958  umgrpredgv  16000  isuspgren  16010  isusgren  16011  ausgrusgrben  16021  usgrf1oedg  16058  uhgr2edg  16059  usgredg3  16067  ushgredgedg  16079  ushgredgedgloop  16081  usgr0  16092  egrsubgr  16116  0grsubgr  16117  vtxdfifiun  16150  edginwlkd  16208  wlk1walkdom  16212  clwwlknon2x  16288  clwwlknonex2lem1  16290  ex-ceil  16325  ex-gcd  16330  bj-charfundcALT  16407  bdceqir  16442  bj-ssom  16534  trilpolemgt1  16646  redcwlpolemeq1  16661