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  3258  sseqtrri  3260  eqsstrrid  3272  sseqtrrdi  3274  difdif2ss  3462  inrab2  3478  dfopg  3858  opid  3878  eqbrtrri  4109  breqtrri  4113  breqtrrdi  4128  opwo0id  4339  pwin  4377  limon  4609  tfis  4679  dfdm2  5269  cnvresid  5401  fores  5566  funcoeqres  5611  f1oprg  5625  fvmbr  5670  fnmptfvd  5747  funopdmsn  5829  fmptpr  5841  fsnunres  5851  idref  5892  riotaeqimp  5991  riotaprop  5992  fo1st  6315  fo2nd  6316  fnmpoovd  6375  ixpsnf1o  6900  phplem4  7036  snnen2og  7040  phplem4on  7049  pw1dc0el  7098  ss1o0el1o  7100  sbthlemi5  7154  eldju  7261  casefun  7278  omp1eomlem  7287  exmidfodomrlemim  7405  caucvgsrlembound  8007  ax0id  8091  1p1e2  9253  1e2m1  9255  2p1e3  9270  3p1e4  9272  4p1e5  9273  5p1e6  9274  6p1e7  9275  7p1e8  9276  8p1e9  9277  div4p1lem1div2  9391  0mnnnnn0  9427  zeo  9578  num0u  9614  numsucc  9643  decsucc  9644  1e0p1  9645  nummac  9648  decsubi  9666  decmul1  9667  decmul10add  9672  6p5lem  9673  10m1e9  9699  5t5e25  9706  6t6e36  9711  8t6e48  9722  decbin3  9745  infrenegsupex  9821  ige3m2fz  10277  fseq1p1m1  10322  fz0tp  10350  fz0to4untppr  10352  1fv  10367  fzo0to42pr  10458  fzosplitpr  10472  fzosplitprm1  10473  fldiv4lem1div2uz2  10559  xnn0nnen  10692  expnegap0  10802  sq4e2t8  10892  3dec  10969  fihashen1  11054  pr0hash2ex  11072  fundm2domnop0  11102  pfxccat3  11308  swrdccat  11309  pfxccatpfx2  11311  swrdccat3blem  11313  swrdccat3b  11314  cats2catd  11343  imi  11454  infxrnegsupex  11817  zsumdc  11938  fsumadd  11960  hashrabrex  12035  ntrivcvgap  12102  fprodmul  12145  fproddivapf  12185  fprodmodd  12195  efsep  12245  3dvds  12418  3dvdsdec  12419  3dvds2dec  12420  flodddiv4  12490  lcmneg  12639  dec2dvds  12977  2exp5  12998  2exp11  13002  ennnfonelem1  13021  nninfdclemp1  13064  ndxid  13099  2strstr1g  13198  srgfcl  13979  isrhm  14165  issubrng  14206  rmodislmod  14358  cnfld0  14578  cnfld1  14579  cnfldplusf  14581  cnfldui  14596  toponrestid  14738  istpsi  14756  distopon  14804  distps  14808  discld  14853  txbas  14975  txdis  14994  txdis1cn  14995  txhmeo  15036  txswaphmeolem  15037  dvmptidcn  15431  dvmptid  15433  sinq34lt0t  15548  loge  15584  2logb9irr  15688  2logb9irrALT  15691  sqrt2cxp2logb9e3  15692  2logb9irrap  15694  lgsdir  15757  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  2lgslem3d1  15822  2lgsoddprmlem3d  15832  2sqlem9  15846  2sqlem10  15847  setsvtx  15895  edgiedgbg  15909  edg0iedg0g  15910  isuhgrm  15915  isushgrm  15916  uhgr0  15929  isupgren  15939  isumgren  15949  umgrpredgv  15991  isuspgren  16001  isusgren  16002  ausgrusgrben  16012  usgrf1oedg  16049  uhgr2edg  16050  usgredg3  16058  ushgredgedg  16070  ushgredgedgloop  16072  usgr0  16083  vtxdfifiun  16108  edginwlkd  16166  wlk1walkdom  16170  clwwlknon2x  16244  clwwlknonex2lem1  16246  ex-ceil  16272  ex-gcd  16277  bj-charfundcALT  16354  bdceqir  16389  bj-ssom  16481  trilpolemgt1  16593  redcwlpolemeq1  16608