Theorem eqcomi 2242

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  eqtr3id  2285  eqtr3di  2286  eqtr4di  2289  eqtr4id  2290  eqeltrri  2312  eleqtrri  2314  eqeltrrid  2326  eleqtrrdi  2332  abid2  2361  abid2f  2418  eqnetrri  2445  neeqtrri  2449  eqsstrri  3281  sseqtrri  3283  eqsstrrid  3295  sseqtrrdi  3297  difdif2ss  3488  inrab2  3506  dfopg  3902  opid  3922  eqbrtrri  4154  breqtrri  4158  breqtrrdi  4173  opwo0id  4391  pwin  4429  limon  4662  tfis  4732  dfdm2  5325  cnvresid  5458  fores  5628  funcoeqres  5673  f1oprg  5688  fvmbr  5734  fnmptfvd  5816  funopdmsn  5898  fmptpr  5910  fsnunres  5920  idref  5965  riotaeqimp  6066  riotaprop  6067  fo1st  6395  fo2nd  6396  fnmpoovd  6455  ixpsnf1o  7023  phplem4  7161  snnen2og  7165  phplem4on  7174  pw1dc0el  7223  ss1o0el1o  7225  sbthlemi5  7284  eldju  7415  casefun  7432  omp1eomlem  7441  exmidfodomrlemim  7560  caucvgsrlembound  8168  ax0id  8252  1p1e2  9431  1e2m1  9433  2p1e3  9448  3p1e4  9450  4p1e5  9451  5p1e6  9452  6p1e7  9453  7p1e8  9454  8p1e9  9455  div4p1lem1div2  9571  0mnnnnn0  9607  zeo  9763  num0u  9799  numsucc  9833  decsucc  9834  1e0p1  9835  nummac  9838  decsubi  9856  decmul1  9857  decmul10add  9862  6p5lem  9863  10m1e9  9889  5t5e25  9896  6t6e36  9901  8t6e48  9912  decbin3  9935  infrenegsupex  10011  ige3m2fz  10472  fseq1p1m1  10519  fz0tp  10547  fz0to4untppr  10549  1fv  10564  fzo0to42pr  10656  fzosplitpr  10670  fzosplitprm1  10671  fldiv4lem1div2uz2  10763  xnn0nnen  10896  expnegap0  11006  sq4e2t8  11096  3dec  11175  fihashen1  11261  pr0hash2ex  11279  fundm2domnop0  11323  pfxccat3  11529  swrdccat  11530  pfxccatpfx2  11532  swrdccat3blem  11534  swrdccat3b  11535  cats2catd  11564  imi  11689  infxrnegsupex  12055  zsumdc  12177  fsumadd  12199  hashrabrex  12274  ntrivcvgap  12341  fprodmul  12384  fproddivapf  12424  fprodmodd  12434  efsep  12484  3dvds  12657  3dvdsdec  12658  3dvds2dec  12659  flodddiv4  12729  lcmneg  12878  dec2dvds  13220  2exp5  13242  2exp11  13246  1259prm  13277  ballotfilemth  13340  ennnfonelem1  13357  nninfdclemp1  13400  ndxid  13435  2strstr1g  13536  srgfcl  14385  isrhm  14575  issubrng  14617  rmodislmod  14798  cnfld0  15018  cnfld1  15019  cnfldplusf  15021  cnfldui  15034  isassa  15112  assamulgscmlem2  15152  toponrestid  15259  istpsi  15277  distopon  15325  distps  15329  discld  15374  txbas  15496  txdis  15515  txdis1cn  15516  txhmeo  15557  txswaphmeolem  15558  dvmptidcn  15952  dvmptid  15954  sinq34lt0t  16070  loge  16108  2logb9irr  16219  2logb9irrALT  16222  sqrt2cxp2logb9e3  16223  2logb9irrap  16225  birthdaylog2  16240  cht2  16288  cht3  16289  chtublem  16307  bclbnd  16319  bposlem6  16328  bposlem8  16330  lgsdir  16371  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  2lgslem3d1  16436  2lgsoddprmlem3d  16446  2sqlem9  16460  2sqlem10  16461  setsvtx  16509  edgiedgbg  16523  edg0iedg0g  16524  isuhgrm  16529  isushgrm  16530  uhgr0  16543  isupgren  16553  isumgren  16563  umgrpredgv  16605  isuspgren  16615  isusgren  16616  ausgrusgrben  16626  usgrf1oedg  16663  uhgr2edg  16664  usgredg3  16672  ushgredgedg  16684  ushgredgedgloop  16686  usgr0  16697  egrsubgr  16721  0grsubgr  16722  vtxdfifiun  16755  edginwlkd  16813  wlk1walkdom  16817  clwwlknon2x  16893  clwwlknonex2lem1  16895  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem5  16950  ex-ceil  16957  ex-gcd  16962  bj-charfundcALT  17052  bdceqir  17087  bj-ssom  17179  trilpolemgt1  17307  redcwlpolemeq1  17323