Theorem eqcomd 2042

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqcomd	⊢ (φ → B = A)

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 ⊢ (φ → A = B)
2		eqcom 2039	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	sylib 127	1 ⊢ (φ → B = A)

Syntax hints:   → wi 4   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqtr2d  2070  eqtr3d  2071  eqtr4d  2072  syl5req  2082  syl6req  2086  sylan9req  2090  eqeltrrd  2112  eleqtrrd  2114  syl5eleqr  2124  syl6eqelr  2126  eqnetrrd  2225  neeqtrrd  2229  dedhb  2704  eqsstr3d  2974  sseqtr4d  2976  syl6eqssr  2990  dfrab3ss  3209  uneqdifeqim  3302  disjsn2  3424  diftpsn3  3496  dfopg  3538  unimax  3605  sndisj  3751  eqbrtrrd  3777  breqtrrd  3781  syl5breqr  3791  syl6eqbrr  3793  class2seteq  3907  opth1  3964  euotd  3982  opelopabsb  3988  tfisi  4253  0nelxp  4315  opeliunxp  4338  euiotaex  4826  iota4  4828  fun2ssres  4886  funimass1  4919  funssfv  5142  fnimapr  5176  fvun1  5182  fmptco  5273  foeqcnvco  5373  f1eqcocnv  5374  f1oiso2  5409  riotass2  5437  riotass  5438  f1ocnvfv3  5444  caovlem2d  5635  f1opw2  5648  sbcopeq1a  5755  csbopeq1a  5756  eloprabi  5764  cnvf1olem  5787  f2ndf  5789  smoiso  5858  nnaword  6020  eqer  6074  uniqs  6100  enq0sym  6415  enq0tr  6417  recexgt0sr  6701  le2tri3i  6923  cnegexlem2  6984  nnpcan  7030  subdi  7178  rereim  7370  cru  7386  divap1d  7558  elz2  8088  zindd  8132  qapne  8350  xrlttri3  8488  fseq1p1m1  8726  fzrevral  8737  nn0disj  8765  fzosplitsnm1  8835  fzosplitprm1  8860  frecuzrdgsuc  8882  frecfzen2  8885  expgt1  8947  leexp2r  8962  replim  9087  cjexp  9121