Theorem eqcomi 2235

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 2233	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

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  10466  fzosplitpr  10480  fzosplitprm1  10481  fldiv4lem1div2uz2  10567  xnn0nnen  10700  expnegap0  10810  sq4e2t8  10900  3dec  10977  fihashen1  11062  pr0hash2ex  11080  fundm2domnop0  11113  pfxccat3  11319  swrdccat  11320  pfxccatpfx2  11322  swrdccat3blem  11324  swrdccat3b  11325  cats2catd  11354  imi  11465  infxrnegsupex  11828  zsumdc  11950  fsumadd  11972  hashrabrex  12047  ntrivcvgap  12114  fprodmul  12157  fproddivapf  12197  fprodmodd  12207  efsep  12257  3dvds  12430  3dvdsdec  12431  3dvds2dec  12432  flodddiv4  12502  lcmneg  12651  dec2dvds  12989  2exp5  13010  2exp11  13014  ennnfonelem1  13033  nninfdclemp1  13076  ndxid  13111  2strstr1g  13210  srgfcl  13992  isrhm  14178  issubrng  14219  rmodislmod  14371  cnfld0  14591  cnfld1  14592  cnfldplusf  14594  cnfldui  14609  toponrestid  14751  istpsi  14769  distopon  14817  distps  14821  discld  14866  txbas  14988  txdis  15007  txdis1cn  15008  txhmeo  15049  txswaphmeolem  15050  dvmptidcn  15444  dvmptid  15446  sinq34lt0t  15561  loge  15597  2logb9irr  15701  2logb9irrALT  15704  sqrt2cxp2logb9e3  15705  2logb9irrap  15707  lgsdir  15770  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgslem3d1  15835  2lgsoddprmlem3d  15845  2sqlem9  15859  2sqlem10  15860  setsvtx  15908  edgiedgbg  15922  edg0iedg0g  15923  isuhgrm  15928  isushgrm  15929  uhgr0  15942  isupgren  15952  isumgren  15962  umgrpredgv  16004  isuspgren  16014  isusgren  16015  ausgrusgrben  16025  usgrf1oedg  16062  uhgr2edg  16063  usgredg3  16071  ushgredgedg  16083  ushgredgedgloop  16085  usgr0  16096  egrsubgr  16120  0grsubgr  16121  vtxdfifiun  16154  edginwlkd  16212  wlk1walkdom  16216  clwwlknon2x  16292  clwwlknonex2lem1  16294  ex-ceil  16344  ex-gcd  16349  bj-charfundcALT  16430  bdceqir  16465  bj-ssom  16557  trilpolemgt1  16669  redcwlpolemeq1  16684