Theorem eqcomi 2200

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqtr2i  2218  eqtr3i  2219  eqtr4i  2220  eqtr3id  2243  eqtr3di  2244  eqtr4di  2247  eqtr4id  2248  eqeltrri  2270  eleqtrri  2272  eqeltrrid  2284  eleqtrrdi  2290  abid2  2317  abid2f  2365  eqnetrri  2392  neeqtrri  2396  eqsstrri  3217  sseqtrri  3219  eqsstrrid  3231  sseqtrrdi  3233  difdif2ss  3421  inrab2  3437  dfopg  3807  opid  3827  eqbrtrri  4057  breqtrri  4061  breqtrrdi  4076  pwin  4318  limon  4550  tfis  4620  dfdm2  5205  cnvresid  5333  fores  5493  funcoeqres  5538  f1oprg  5551  fnmptfvd  5669  fmptpr  5757  fsnunres  5767  idref  5806  riotaprop  5904  fo1st  6224  fo2nd  6225  fnmpoovd  6282  ixpsnf1o  6804  phplem4  6925  snnen2og  6929  phplem4on  6937  pw1dc0el  6981  ss1o0el1o  6983  sbthlemi5  7036  eldju  7143  casefun  7160  omp1eomlem  7169  exmidfodomrlemim  7280  caucvgsrlembound  7878  ax0id  7962  1p1e2  9124  1e2m1  9126  2p1e3  9141  3p1e4  9143  4p1e5  9144  5p1e6  9145  6p1e7  9146  7p1e8  9147  8p1e9  9148  div4p1lem1div2  9262  0mnnnnn0  9298  zeo  9448  num0u  9484  numsucc  9513  decsucc  9514  1e0p1  9515  nummac  9518  decsubi  9536  decmul1  9537  decmul10add  9542  6p5lem  9543  10m1e9  9569  5t5e25  9576  6t6e36  9581  8t6e48  9592  decbin3  9615  infrenegsupex  9685  ige3m2fz  10141  fseq1p1m1  10186  fz0tp  10214  fz0to4untppr  10216  1fv  10231  fzo0to42pr  10313  fzosplitprm1  10327  fldiv4lem1div2uz2  10413  xnn0nnen  10546  expnegap0  10656  sq4e2t8  10746  3dec  10823  fihashen1  10908  pr0hash2ex  10924  imi  11082  infxrnegsupex  11445  zsumdc  11566  fsumadd  11588  hashrabrex  11663  ntrivcvgap  11730  fprodmul  11773  fproddivapf  11813  fprodmodd  11823  efsep  11873  3dvds  12046  3dvdsdec  12047  3dvds2dec  12048  flodddiv4  12118  lcmneg  12267  dec2dvds  12605  2exp5  12626  2exp11  12630  ennnfonelem1  12649  nninfdclemp1  12692  ndxid  12727  2strstr1g  12824  srgfcl  13605  isrhm  13790  issubrng  13831  rmodislmod  13983  cnfld0  14203  cnfld1  14204  cnfldplusf  14206  cnfldui  14221  toponrestid  14341  istpsi  14359  distopon  14407  distps  14411  discld  14456  txbas  14578  txdis  14597  txdis1cn  14598  txhmeo  14639  txswaphmeolem  14640  dvmptidcn  15034  dvmptid  15036  sinq34lt0t  15151  loge  15187  2logb9irr  15291  2logb9irrALT  15294  sqrt2cxp2logb9e3  15295  2logb9irrap  15297  lgsdir  15360  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2lgsoddprmlem3d  15435  2sqlem9  15449  2sqlem10  15450  ex-ceil  15456  ex-gcd  15461  bj-charfundcALT  15539  bdceqir  15574  bj-ssom  15666  trilpolemgt1  15770  redcwlpolemeq1  15785