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  6414  enq0tr  6416  recexgt0sr  6681  le2tri3i  6903  cnegexlem2  6964  nnpcan  7010  subdi  7158  rereim  7350  cru  7366  divap1d  7538  elz2  8068  zindd  8112  qapne  8330  xrlttri3  8468  fseq1p1m1  8706  fzrevral  8717  nn0disj  8745  fzosplitsnm1  8815  fzosplitprm1  8840  frecuzrdgsuc  8862  frecfzen2  8865  expgt1  8927  leexp2r  8942  replim  9067  cjexp  9101