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  4153  breqtrri  4157  breqtrrdi  4172  opwo0id  4389  pwin  4427  limon  4660  tfis  4730  dfdm2  5322  cnvresid  5455  fores  5625  funcoeqres  5670  f1oprg  5685  fvmbr  5731  fnmptfvd  5813  funopdmsn  5895  fmptpr  5907  fsnunres  5917  idref  5962  riotaeqimp  6063  riotaprop  6064  fo1st  6391  fo2nd  6392  fnmpoovd  6451  ixpsnf1o  7018  phplem4  7156  snnen2og  7160  phplem4on  7169  pw1dc0el  7218  ss1o0el1o  7220  sbthlemi5  7278  eldju  7409  casefun  7426  omp1eomlem  7435  exmidfodomrlemim  7554  caucvgsrlembound  8162  ax0id  8246  1p1e2  9424  1e2m1  9426  2p1e3  9441  3p1e4  9443  4p1e5  9444  5p1e6  9445  6p1e7  9446  7p1e8  9447  8p1e9  9448  div4p1lem1div2  9564  0mnnnnn0  9600  zeo  9756  num0u  9792  numsucc  9826  decsucc  9827  1e0p1  9828  nummac  9831  decsubi  9849  decmul1  9850  decmul10add  9855  6p5lem  9856  10m1e9  9882  5t5e25  9889  6t6e36  9894  8t6e48  9905  decbin3  9928  infrenegsupex  10004  ige3m2fz  10465  fseq1p1m1  10512  fz0tp  10540  fz0to4untppr  10542  1fv  10557  fzo0to42pr  10649  fzosplitpr  10663  fzosplitprm1  10664  fldiv4lem1div2uz2  10755  xnn0nnen  10888  expnegap0  10998  sq4e2t8  11088  3dec  11167  fihashen1  11253  pr0hash2ex  11271  fundm2domnop0  11315  pfxccat3  11521  swrdccat  11522  pfxccatpfx2  11524  swrdccat3blem  11526  swrdccat3b  11527  cats2catd  11556  imi  11681  infxrnegsupex  12047  zsumdc  12169  fsumadd  12191  hashrabrex  12266  ntrivcvgap  12333  fprodmul  12376  fproddivapf  12416  fprodmodd  12426  efsep  12476  3dvds  12649  3dvdsdec  12650  3dvds2dec  12651  flodddiv4  12721  lcmneg  12870  dec2dvds  13212  2exp5  13234  2exp11  13238  1259prm  13269  ballotfilemth  13332  ennnfonelem1  13349  nninfdclemp1  13392  ndxid  13427  2strstr1g  13527  srgfcl  14328  isrhm  14516  issubrng  14558  rmodislmod  14739  cnfld0  14959  cnfld1  14960  cnfldplusf  14962  cnfldui  14975  isassa  15053  assamulgscmlem2  15093  toponrestid  15174  istpsi  15192  distopon  15240  distps  15244  discld  15289  txbas  15411  txdis  15430  txdis1cn  15431  txhmeo  15472  txswaphmeolem  15473  dvmptidcn  15867  dvmptid  15869  sinq34lt0t  15985  loge  16021  2logb9irr  16129  2logb9irrALT  16132  sqrt2cxp2logb9e3  16133  2logb9irrap  16135  birthdaylog2  16150  cht2  16198  cht3  16199  chtublem  16217  bclbnd  16229  lgsdir  16276  2lgslem3a  16334  2lgslem3b  16335  2lgslem3c  16336  2lgslem3d  16337  2lgslem3d1  16341  2lgsoddprmlem3d  16351  2sqlem9  16365  2sqlem10  16366  setsvtx  16414  edgiedgbg  16428  edg0iedg0g  16429  isuhgrm  16434  isushgrm  16435  uhgr0  16448  isupgren  16458  isumgren  16468  umgrpredgv  16510  isuspgren  16520  isusgren  16521  ausgrusgrben  16531  usgrf1oedg  16568  uhgr2edg  16569  usgredg3  16577  ushgredgedg  16589  ushgredgedgloop  16591  usgr0  16602  egrsubgr  16626  0grsubgr  16627  vtxdfifiun  16660  edginwlkd  16718  wlk1walkdom  16722  clwwlknon2x  16798  clwwlknonex2lem1  16800  konigsberglem1  16851  konigsberglem2  16852  konigsberglem3  16853  konigsberglem5  16855  ex-ceil  16862  ex-gcd  16867  bj-charfundcALT  16957  bdceqir  16992  bj-ssom  17084  trilpolemgt1  17210  redcwlpolemeq1  17226