Theorem eqcomi 2209

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-ext 2187

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

This theorem is referenced by:  eqtr2i  2227  eqtr3i  2228  eqtr4i  2229  eqtr3id  2252  eqtr3di  2253  eqtr4di  2256  eqtr4id  2257  eqeltrri  2279  eleqtrri  2281  eqeltrrid  2293  eleqtrrdi  2299  abid2  2326  abid2f  2374  eqnetrri  2401  neeqtrri  2405  eqsstrri  3226  sseqtrri  3228  eqsstrrid  3240  sseqtrrdi  3242  difdif2ss  3430  inrab2  3446  dfopg  3817  opid  3837  eqbrtrri  4067  breqtrri  4071  breqtrrdi  4086  opwo0id  4293  pwin  4329  limon  4561  tfis  4631  dfdm2  5217  cnvresid  5348  fores  5508  funcoeqres  5553  f1oprg  5566  fnmptfvd  5684  funopdmsn  5764  fmptpr  5776  fsnunres  5786  idref  5825  riotaprop  5923  fo1st  6243  fo2nd  6244  fnmpoovd  6301  ixpsnf1o  6823  phplem4  6952  snnen2og  6956  phplem4on  6964  pw1dc0el  7008  ss1o0el1o  7010  sbthlemi5  7063  eldju  7170  casefun  7187  omp1eomlem  7196  exmidfodomrlemim  7309  caucvgsrlembound  7907  ax0id  7991  1p1e2  9153  1e2m1  9155  2p1e3  9170  3p1e4  9172  4p1e5  9173  5p1e6  9174  6p1e7  9175  7p1e8  9176  8p1e9  9177  div4p1lem1div2  9291  0mnnnnn0  9327  zeo  9478  num0u  9514  numsucc  9543  decsucc  9544  1e0p1  9545  nummac  9548  decsubi  9566  decmul1  9567  decmul10add  9572  6p5lem  9573  10m1e9  9599  5t5e25  9606  6t6e36  9611  8t6e48  9622  decbin3  9645  infrenegsupex  9715  ige3m2fz  10171  fseq1p1m1  10216  fz0tp  10244  fz0to4untppr  10246  1fv  10261  fzo0to42pr  10349  fzosplitprm1  10363  fldiv4lem1div2uz2  10449  xnn0nnen  10582  expnegap0  10692  sq4e2t8  10782  3dec  10859  fihashen1  10944  pr0hash2ex  10960  fundm2domnop0  10990  imi  11211  infxrnegsupex  11574  zsumdc  11695  fsumadd  11717  hashrabrex  11792  ntrivcvgap  11859  fprodmul  11902  fproddivapf  11942  fprodmodd  11952  efsep  12002  3dvds  12175  3dvdsdec  12176  3dvds2dec  12177  flodddiv4  12247  lcmneg  12396  dec2dvds  12734  2exp5  12755  2exp11  12759  ennnfonelem1  12778  nninfdclemp1  12821  ndxid  12856  2strstr1g  12954  srgfcl  13735  isrhm  13920  issubrng  13961  rmodislmod  14113  cnfld0  14333  cnfld1  14334  cnfldplusf  14336  cnfldui  14351  toponrestid  14493  istpsi  14511  distopon  14559  distps  14563  discld  14608  txbas  14730  txdis  14749  txdis1cn  14750  txhmeo  14791  txswaphmeolem  14792  dvmptidcn  15186  dvmptid  15188  sinq34lt0t  15303  loge  15339  2logb9irr  15443  2logb9irrALT  15446  sqrt2cxp2logb9e3  15447  2logb9irrap  15449  lgsdir  15512  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3d1  15577  2lgsoddprmlem3d  15587  2sqlem9  15601  2sqlem10  15602  ex-ceil  15662  ex-gcd  15667  bj-charfundcALT  15745  bdceqir  15780  bj-ssom  15872  trilpolemgt1  15978  redcwlpolemeq1  15993