Theorem eqcomi 2236

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  eqtr2i  2254  eqtr3i  2255  eqtr4i  2256  eqtr3id  2279  eqtr3di  2280  eqtr4di  2283  eqtr4id  2284  eqeltrri  2306  eleqtrri  2308  eqeltrrid  2320  eleqtrrdi  2326  abid2  2355  abid2f  2410  eqnetrri  2437  neeqtrri  2441  eqsstrri  3270  sseqtrri  3272  eqsstrrid  3284  sseqtrrdi  3286  difdif2ss  3477  inrab2  3493  dfopg  3880  opid  3900  eqbrtrri  4131  breqtrri  4135  breqtrrdi  4150  opwo0id  4364  pwin  4402  limon  4634  tfis  4704  dfdm2  5296  cnvresid  5429  fores  5599  funcoeqres  5644  f1oprg  5659  fvmbr  5704  fnmptfvd  5781  funopdmsn  5863  fmptpr  5875  fsnunres  5885  idref  5928  riotaeqimp  6027  riotaprop  6028  fo1st  6350  fo2nd  6351  fnmpoovd  6410  ixpsnf1o  6970  phplem4  7108  snnen2og  7112  phplem4on  7121  pw1dc0el  7170  ss1o0el1o  7172  sbthlemi5  7230  eldju  7358  casefun  7375  omp1eomlem  7384  exmidfodomrlemim  7503  caucvgsrlembound  8108  ax0id  8192  1p1e2  9353  1e2m1  9355  2p1e3  9370  3p1e4  9372  4p1e5  9373  5p1e6  9374  6p1e7  9375  7p1e8  9376  8p1e9  9377  div4p1lem1div2  9491  0mnnnnn0  9527  zeo  9682  num0u  9718  numsucc  9747  decsucc  9748  1e0p1  9749  nummac  9752  decsubi  9770  decmul1  9771  decmul10add  9776  6p5lem  9777  10m1e9  9803  5t5e25  9810  6t6e36  9815  8t6e48  9826  decbin3  9849  infrenegsupex  9925  ige3m2fz  10382  fseq1p1m1  10427  fz0tp  10455  fz0to4untppr  10457  1fv  10472  fzo0to42pr  10564  fzosplitpr  10578  fzosplitprm1  10579  fldiv4lem1div2uz2  10665  xnn0nnen  10798  expnegap0  10908  sq4e2t8  10998  3dec  11075  fihashen1  11160  pr0hash2ex  11178  fundm2domnop0  11216  pfxccat3  11422  swrdccat  11423  pfxccatpfx2  11425  swrdccat3blem  11427  swrdccat3b  11428  cats2catd  11457  imi  11581  infxrnegsupex  11944  zsumdc  12066  fsumadd  12088  hashrabrex  12163  ntrivcvgap  12230  fprodmul  12273  fproddivapf  12313  fprodmodd  12323  efsep  12373  3dvds  12546  3dvdsdec  12547  3dvds2dec  12548  flodddiv4  12618  lcmneg  12767  dec2dvds  13105  2exp5  13126  2exp11  13130  ennnfonelem1  13150  nninfdclemp1  13193  ndxid  13228  2strstr1g  13327  srgfcl  14109  isrhm  14295  issubrng  14336  rmodislmod  14491  cnfld0  14711  cnfld1  14712  cnfldplusf  14714  cnfldui  14729  toponrestid  14878  istpsi  14896  distopon  14944  distps  14948  discld  14993  txbas  15115  txdis  15134  txdis1cn  15135  txhmeo  15176  txswaphmeolem  15177  dvmptidcn  15571  dvmptid  15573  sinq34lt0t  15688  loge  15724  2logb9irr  15828  2logb9irrALT  15831  sqrt2cxp2logb9e3  15832  2logb9irrap  15834  lgsdir  15900  2lgslem3a  15958  2lgslem3b  15959  2lgslem3c  15960  2lgslem3d  15961  2lgslem3d1  15965  2lgsoddprmlem3d  15975  2sqlem9  15989  2sqlem10  15990  setsvtx  16038  edgiedgbg  16052  edg0iedg0g  16053  isuhgrm  16058  isushgrm  16059  uhgr0  16072  isupgren  16082  isumgren  16092  umgrpredgv  16134  isuspgren  16144  isusgren  16145  ausgrusgrben  16155  usgrf1oedg  16192  uhgr2edg  16193  usgredg3  16201  ushgredgedg  16213  ushgredgedgloop  16215  usgr0  16226  egrsubgr  16250  0grsubgr  16251  vtxdfifiun  16284  edginwlkd  16342  wlk1walkdom  16346  clwwlknon2x  16422  clwwlknonex2lem1  16424  konigsberglem1  16475  konigsberglem2  16476  konigsberglem3  16477  konigsberglem5  16479  ex-ceil  16486  ex-gcd  16491  bj-charfundcALT  16571  bdceqir  16606  bj-ssom  16698  trilpolemgt1  16815  redcwlpolemeq1  16831