Theorem eqcomi 2238

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2216

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

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  eqtr3id  2281  eqtr3di  2282  eqtr4di  2285  eqtr4id  2286  eqeltrri  2308  eleqtrri  2310  eqeltrrid  2322  eleqtrrdi  2328  abid2  2357  abid2f  2412  eqnetrri  2439  neeqtrri  2443  eqsstrri  3275  sseqtrri  3277  eqsstrrid  3289  sseqtrrdi  3291  difdif2ss  3482  inrab2  3498  dfopg  3886  opid  3906  eqbrtrri  4137  breqtrri  4141  breqtrrdi  4156  opwo0id  4370  pwin  4408  limon  4640  tfis  4710  dfdm2  5302  cnvresid  5435  fores  5605  funcoeqres  5650  f1oprg  5665  fvmbr  5710  fnmptfvd  5787  funopdmsn  5869  fmptpr  5881  fsnunres  5891  idref  5935  riotaeqimp  6036  riotaprop  6037  fo1st  6364  fo2nd  6365  fnmpoovd  6424  ixpsnf1o  6984  phplem4  7122  snnen2og  7126  phplem4on  7135  pw1dc0el  7184  ss1o0el1o  7186  sbthlemi5  7244  eldju  7372  casefun  7389  omp1eomlem  7398  exmidfodomrlemim  7517  caucvgsrlembound  8125  ax0id  8209  1p1e2  9371  1e2m1  9373  2p1e3  9388  3p1e4  9390  4p1e5  9391  5p1e6  9392  6p1e7  9393  7p1e8  9394  8p1e9  9395  div4p1lem1div2  9509  0mnnnnn0  9545  zeo  9701  num0u  9737  numsucc  9766  decsucc  9767  1e0p1  9768  nummac  9771  decsubi  9789  decmul1  9790  decmul10add  9795  6p5lem  9796  10m1e9  9822  5t5e25  9829  6t6e36  9834  8t6e48  9845  decbin3  9868  infrenegsupex  9944  ige3m2fz  10403  fseq1p1m1  10450  fz0tp  10478  fz0to4untppr  10480  1fv  10495  fzo0to42pr  10587  fzosplitpr  10601  fzosplitprm1  10602  fldiv4lem1div2uz2  10690  xnn0nnen  10823  expnegap0  10933  sq4e2t8  11023  3dec  11101  fihashen1  11187  pr0hash2ex  11205  fundm2domnop0  11245  pfxccat3  11451  swrdccat  11452  pfxccatpfx2  11454  swrdccat3blem  11456  swrdccat3b  11457  cats2catd  11486  imi  11610  infxrnegsupex  11973  zsumdc  12095  fsumadd  12117  hashrabrex  12192  ntrivcvgap  12259  fprodmul  12302  fproddivapf  12342  fprodmodd  12352  efsep  12402  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  flodddiv4  12647  lcmneg  12796  dec2dvds  13134  2exp5  13155  2exp11  13159  ballotfilemth  13225  ennnfonelem1  13242  nninfdclemp1  13285  ndxid  13320  2strstr1g  13419  srgfcl  14201  isrhm  14388  issubrng  14430  rmodislmod  14611  cnfld0  14831  cnfld1  14832  cnfldplusf  14834  cnfldui  14849  toponrestid  14998  istpsi  15016  distopon  15064  distps  15068  discld  15113  txbas  15235  txdis  15254  txdis1cn  15255  txhmeo  15296  txswaphmeolem  15297  dvmptidcn  15691  dvmptid  15693  sinq34lt0t  15808  loge  15844  2logb9irr  15948  2logb9irrALT  15951  sqrt2cxp2logb9e3  15952  2logb9irrap  15954  lgsdir  16020  2lgslem3a  16078  2lgslem3b  16079  2lgslem3c  16080  2lgslem3d  16081  2lgslem3d1  16085  2lgsoddprmlem3d  16095  2sqlem9  16109  2sqlem10  16110  setsvtx  16158  edgiedgbg  16172  edg0iedg0g  16173  isuhgrm  16178  isushgrm  16179  uhgr0  16192  isupgren  16202  isumgren  16212  umgrpredgv  16254  isuspgren  16264  isusgren  16265  ausgrusgrben  16275  usgrf1oedg  16312  uhgr2edg  16313  usgredg3  16321  ushgredgedg  16333  ushgredgedgloop  16335  usgr0  16346  egrsubgr  16370  0grsubgr  16371  vtxdfifiun  16404  edginwlkd  16462  wlk1walkdom  16466  clwwlknon2x  16542  clwwlknonex2lem1  16544  konigsberglem1  16595  konigsberglem2  16596  konigsberglem3  16597  konigsberglem5  16599  ex-ceil  16606  ex-gcd  16611  bj-charfundcALT  16691  bdceqir  16726  bj-ssom  16818  trilpolemgt1  16935  redcwlpolemeq1  16951