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  3855  opid  3875  eqbrtrri  4106  breqtrri  4110  breqtrrdi  4125  opwo0id  4335  pwin  4373  limon  4605  tfis  4675  dfdm2  5263  cnvresid  5395  fores  5560  funcoeqres  5605  f1oprg  5619  fvmbr  5664  fnmptfvd  5741  funopdmsn  5823  fmptpr  5835  fsnunres  5845  idref  5886  riotaeqimp  5985  riotaprop  5986  fo1st  6309  fo2nd  6310  fnmpoovd  6367  ixpsnf1o  6891  phplem4  7024  snnen2og  7028  phplem4on  7037  pw1dc0el  7084  ss1o0el1o  7086  sbthlemi5  7139  eldju  7246  casefun  7263  omp1eomlem  7272  exmidfodomrlemim  7390  caucvgsrlembound  7992  ax0id  8076  1p1e2  9238  1e2m1  9240  2p1e3  9255  3p1e4  9257  4p1e5  9258  5p1e6  9259  6p1e7  9260  7p1e8  9261  8p1e9  9262  div4p1lem1div2  9376  0mnnnnn0  9412  zeo  9563  num0u  9599  numsucc  9628  decsucc  9629  1e0p1  9630  nummac  9633  decsubi  9651  decmul1  9652  decmul10add  9657  6p5lem  9658  10m1e9  9684  5t5e25  9691  6t6e36  9696  8t6e48  9707  decbin3  9730  infrenegsupex  9801  ige3m2fz  10257  fseq1p1m1  10302  fz0tp  10330  fz0to4untppr  10332  1fv  10347  fzo0to42pr  10438  fzosplitprm1  10452  fldiv4lem1div2uz2  10538  xnn0nnen  10671  expnegap0  10781  sq4e2t8  10871  3dec  10948  fihashen1  11033  pr0hash2ex  11050  fundm2domnop0  11080  pfxccat3  11281  swrdccat  11282  pfxccatpfx2  11284  swrdccat3blem  11286  swrdccat3b  11287  cats2catd  11316  imi  11426  infxrnegsupex  11789  zsumdc  11910  fsumadd  11932  hashrabrex  12007  ntrivcvgap  12074  fprodmul  12117  fproddivapf  12157  fprodmodd  12167  efsep  12217  3dvds  12390  3dvdsdec  12391  3dvds2dec  12392  flodddiv4  12462  lcmneg  12611  dec2dvds  12949  2exp5  12970  2exp11  12974  ennnfonelem1  12993  nninfdclemp1  13036  ndxid  13071  2strstr1g  13170  srgfcl  13951  isrhm  14137  issubrng  14178  rmodislmod  14330  cnfld0  14550  cnfld1  14551  cnfldplusf  14553  cnfldui  14568  toponrestid  14710  istpsi  14728  distopon  14776  distps  14780  discld  14825  txbas  14947  txdis  14966  txdis1cn  14967  txhmeo  15008  txswaphmeolem  15009  dvmptidcn  15403  dvmptid  15405  sinq34lt0t  15520  loge  15556  2logb9irr  15660  2logb9irrALT  15663  sqrt2cxp2logb9e3  15664  2logb9irrap  15666  lgsdir  15729  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgslem3d1  15794  2lgsoddprmlem3d  15804  2sqlem9  15818  2sqlem10  15819  setsvtx  15867  edgiedgbg  15880  edg0iedg0g  15881  isuhgrm  15886  isushgrm  15887  uhgr0  15900  isupgren  15910  isumgren  15920  umgrpredgv  15960  isuspgren  15970  isusgren  15971  ausgrusgrben  15981  usgrf1oedg  16018  uhgr2edg  16019  usgredg3  16027  ushgredgedg  16039  ushgredgedgloop  16041  vtxdfifiun  16056  edginwlkd  16096  wlk1walkdom  16100  ex-ceil  16145  ex-gcd  16150  bj-charfundcALT  16227  bdceqir  16262  bj-ssom  16354  trilpolemgt1  16467  redcwlpolemeq1  16482