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  4335  pwin  4373  limon  4605  tfis  4675  dfdm2  5263  cnvresid  5395  fores  5560  funcoeqres  5605  f1oprg  5619  fvmbr  5664  fnmptfvd  5741  funopdmsn  5823  fmptpr  5835  fsnunres  5845  idref  5886  riotaeqimp  5985  riotaprop  5986  fo1st  6309  fo2nd  6310  fnmpoovd  6367  ixpsnf1o  6891  phplem4  7024  snnen2og  7028  phplem4on  7037  pw1dc0el  7081  ss1o0el1o  7083  sbthlemi5  7136  eldju  7243  casefun  7260  omp1eomlem  7269  exmidfodomrlemim  7387  caucvgsrlembound  7989  ax0id  8073  1p1e2  9235  1e2m1  9237  2p1e3  9252  3p1e4  9254  4p1e5  9255  5p1e6  9256  6p1e7  9257  7p1e8  9258  8p1e9  9259  div4p1lem1div2  9373  0mnnnnn0  9409  zeo  9560  num0u  9596  numsucc  9625  decsucc  9626  1e0p1  9627  nummac  9630  decsubi  9648  decmul1  9649  decmul10add  9654  6p5lem  9655  10m1e9  9681  5t5e25  9688  6t6e36  9693  8t6e48  9704  decbin3  9727  infrenegsupex  9797  ige3m2fz  10253  fseq1p1m1  10298  fz0tp  10326  fz0to4untppr  10328  1fv  10343  fzo0to42pr  10434  fzosplitprm1  10448  fldiv4lem1div2uz2  10534  xnn0nnen  10667  expnegap0  10777  sq4e2t8  10867  3dec  10944  fihashen1  11029  pr0hash2ex  11045  fundm2domnop0  11075  pfxccat3  11274  swrdccat  11275  pfxccatpfx2  11277  swrdccat3blem  11279  swrdccat3b  11280  cats2catd  11309  imi  11419  infxrnegsupex  11782  zsumdc  11903  fsumadd  11925  hashrabrex  12000  ntrivcvgap  12067  fprodmul  12110  fproddivapf  12150  fprodmodd  12160  efsep  12210  3dvds  12383  3dvdsdec  12384  3dvds2dec  12385  flodddiv4  12455  lcmneg  12604  dec2dvds  12942  2exp5  12963  2exp11  12967  ennnfonelem1  12986  nninfdclemp1  13029  ndxid  13064  2strstr1g  13163  srgfcl  13944  isrhm  14130  issubrng  14171  rmodislmod  14323  cnfld0  14543  cnfld1  14544  cnfldplusf  14546  cnfldui  14561  toponrestid  14703  istpsi  14721  distopon  14769  distps  14773  discld  14818  txbas  14940  txdis  14959  txdis1cn  14960  txhmeo  15001  txswaphmeolem  15002  dvmptidcn  15396  dvmptid  15398  sinq34lt0t  15513  loge  15549  2logb9irr  15653  2logb9irrALT  15656  sqrt2cxp2logb9e3  15657  2logb9irrap  15659  lgsdir  15722  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgslem3d1  15787  2lgsoddprmlem3d  15797  2sqlem9  15811  2sqlem10  15812  setsvtx  15860  edgiedgbg  15873  edg0iedg0g  15874  isuhgrm  15879  isushgrm  15880  uhgr0  15893  isupgren  15903  isumgren  15913  umgrpredgv  15953  isuspgren  15963  isusgren  15964  ausgrusgrben  15974  usgrf1oedg  16011  uhgr2edg  16012  usgredg3  16020  ushgredgedg  16032  ushgredgedgloop  16034  edginwlkd  16076  wlk1walkdom  16080  ex-ceil  16114  ex-gcd  16119  bj-charfundcALT  16196  bdceqir  16231  bj-ssom  16323  trilpolemgt1  16437  redcwlpolemeq1  16452