Theorem eqcomi 2233

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  eqtr3id  2276  eqtr3di  2277  eqtr4di  2280  eqtr4id  2281  eqeltrri  2303  eleqtrri  2305  eqeltrrid  2317  eleqtrrdi  2323  abid2  2350  abid2f  2398  eqnetrri  2425  neeqtrri  2429  eqsstrri  3257  sseqtrri  3259  eqsstrrid  3271  sseqtrrdi  3273  difdif2ss  3461  inrab2  3477  dfopg  3855  opid  3875  eqbrtrri  4106  breqtrri  4110  breqtrrdi  4125  opwo0id  4336  pwin  4374  limon  4606  tfis  4676  dfdm2  5266  cnvresid  5398  fores  5563  funcoeqres  5608  f1oprg  5622  fvmbr  5667  fnmptfvd  5744  funopdmsn  5826  fmptpr  5838  fsnunres  5848  idref  5889  riotaeqimp  5988  riotaprop  5989  fo1st  6312  fo2nd  6313  fnmpoovd  6372  ixpsnf1o  6896  phplem4  7029  snnen2og  7033  phplem4on  7042  pw1dc0el  7089  ss1o0el1o  7091  sbthlemi5  7144  eldju  7251  casefun  7268  omp1eomlem  7277  exmidfodomrlemim  7395  caucvgsrlembound  7997  ax0id  8081  1p1e2  9243  1e2m1  9245  2p1e3  9260  3p1e4  9262  4p1e5  9263  5p1e6  9264  6p1e7  9265  7p1e8  9266  8p1e9  9267  div4p1lem1div2  9381  0mnnnnn0  9417  zeo  9568  num0u  9604  numsucc  9633  decsucc  9634  1e0p1  9635  nummac  9638  decsubi  9656  decmul1  9657  decmul10add  9662  6p5lem  9663  10m1e9  9689  5t5e25  9696  6t6e36  9701  8t6e48  9712  decbin3  9735  infrenegsupex  9806  ige3m2fz  10262  fseq1p1m1  10307  fz0tp  10335  fz0to4untppr  10337  1fv  10352  fzo0to42pr  10443  fzosplitprm1  10457  fldiv4lem1div2uz2  10543  xnn0nnen  10676  expnegap0  10786  sq4e2t8  10876  3dec  10953  fihashen1  11038  pr0hash2ex  11055  fundm2domnop0  11085  pfxccat3  11287  swrdccat  11288  pfxccatpfx2  11290  swrdccat3blem  11292  swrdccat3b  11293  cats2catd  11322  imi  11432  infxrnegsupex  11795  zsumdc  11916  fsumadd  11938  hashrabrex  12013  ntrivcvgap  12080  fprodmul  12123  fproddivapf  12163  fprodmodd  12173  efsep  12223  3dvds  12396  3dvdsdec  12397  3dvds2dec  12398  flodddiv4  12468  lcmneg  12617  dec2dvds  12955  2exp5  12976  2exp11  12980  ennnfonelem1  12999  nninfdclemp1  13042  ndxid  13077  2strstr1g  13176  srgfcl  13957  isrhm  14143  issubrng  14184  rmodislmod  14336  cnfld0  14556  cnfld1  14557  cnfldplusf  14559  cnfldui  14574  toponrestid  14716  istpsi  14734  distopon  14782  distps  14786  discld  14831  txbas  14953  txdis  14972  txdis1cn  14973  txhmeo  15014  txswaphmeolem  15015  dvmptidcn  15409  dvmptid  15411  sinq34lt0t  15526  loge  15562  2logb9irr  15666  2logb9irrALT  15669  sqrt2cxp2logb9e3  15670  2logb9irrap  15672  lgsdir  15735  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  2lgslem3d1  15800  2lgsoddprmlem3d  15810  2sqlem9  15824  2sqlem10  15825  setsvtx  15873  edgiedgbg  15886  edg0iedg0g  15887  isuhgrm  15892  isushgrm  15893  uhgr0  15906  isupgren  15916  isumgren  15926  umgrpredgv  15966  isuspgren  15976  isusgren  15977  ausgrusgrben  15987  usgrf1oedg  16024  uhgr2edg  16025  usgredg3  16033  ushgredgedg  16045  ushgredgedgloop  16047  usgr0  16058  vtxdfifiun  16083  edginwlkd  16127  wlk1walkdom  16131  ex-ceil  16199  ex-gcd  16204  bj-charfundcALT  16281  bdceqir  16316  bj-ssom  16408  trilpolemgt1  16521  redcwlpolemeq1  16536