Theorem eqcomi 2200

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2198	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

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  7282  caucvgsrlembound  7880  ax0id  7964  1p1e2  9126  1e2m1  9128  2p1e3  9143  3p1e4  9145  4p1e5  9146  5p1e6  9147  6p1e7  9148  7p1e8  9149  8p1e9  9150  div4p1lem1div2  9264  0mnnnnn0  9300  zeo  9450  num0u  9486  numsucc  9515  decsucc  9516  1e0p1  9517  nummac  9520  decsubi  9538  decmul1  9539  decmul10add  9544  6p5lem  9545  10m1e9  9571  5t5e25  9578  6t6e36  9583  8t6e48  9594  decbin3  9617  infrenegsupex  9687  ige3m2fz  10143  fseq1p1m1  10188  fz0tp  10216  fz0to4untppr  10218  1fv  10233  fzo0to42pr  10315  fzosplitprm1  10329  fldiv4lem1div2uz2  10415  xnn0nnen  10548  expnegap0  10658  sq4e2t8  10748  3dec  10825  fihashen1  10910  pr0hash2ex  10926  imi  11084  infxrnegsupex  11447  zsumdc  11568  fsumadd  11590  hashrabrex  11665  ntrivcvgap  11732  fprodmul  11775  fproddivapf  11815  fprodmodd  11825  efsep  11875  3dvds  12048  3dvdsdec  12049  3dvds2dec  12050  flodddiv4  12120  lcmneg  12269  dec2dvds  12607  2exp5  12628  2exp11  12632  ennnfonelem1  12651  nninfdclemp1  12694  ndxid  12729  2strstr1g  12826  srgfcl  13607  isrhm  13792  issubrng  13833  rmodislmod  13985  cnfld0  14205  cnfld1  14206  cnfldplusf  14208  cnfldui  14223  toponrestid  14365  istpsi  14383  distopon  14431  distps  14435  discld  14480  txbas  14602  txdis  14621  txdis1cn  14622  txhmeo  14663  txswaphmeolem  14664  dvmptidcn  15058  dvmptid  15060  sinq34lt0t  15175  loge  15211  2logb9irr  15315  2logb9irrALT  15318  sqrt2cxp2logb9e3  15319  2logb9irrap  15321  lgsdir  15384  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3d1  15449  2lgsoddprmlem3d  15459  2sqlem9  15473  2sqlem10  15474  ex-ceil  15480  ex-gcd  15485  bj-charfundcALT  15563  bdceqir  15598  bj-ssom  15690  trilpolemgt1  15796  redcwlpolemeq1  15811