Theorem eqeltrrd 2156

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eqeltrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrrd.2	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrrd	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2086	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2155	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  3eltr3d  2161  xpexr2m  4782  funimaexg  5003  fvmptdv2  5281  ffvresb  5349  2ndrn  5829  1st2ndbr  5830  elopabi  5841  cnvf1olem  5865  dftpos4  5901  tfrlemibxssdm  5964  nnmordi  6112  th3qlem1  6231  infiexmid  6362  onunsnss  6383  fnfi  6388  ordiso2  6446  archnqq  6607  prarloclemarch2  6609  enq0tr  6624  nqnq0  6631  addcmpblnq0  6633  mulcmpblnq0  6634  mulcanenq0ec  6635  addclnq0  6641  mulclnq0  6642  nqpnq0nq  6643  nq0m0r  6646  distrnq0  6649  addassnq0lemcl  6651  prarloclemlt  6683  prarloclem5  6690  distrlem4prl  6774  distrlem4pru  6775  ltexprlemm  6790  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  cauappcvgprlemladdru  6846  prsrlem1  6919  mulgt0sr  6954  cnegexlem2  7284  subf  7310  resubcl  7372  negcon1ad  7414  subeq0bd  7483  rimul  7685  rereim  7686  nn0nnaddcl  8319  elnn0nn  8330  zaddcllemneg  8390  zsubcl  8392  zrevaddcl  8401  elz2  8419  zdiv  8435  peano5uzti  8455  peano2uzr  8673  uzaddcl  8674  divfnzn  8706  qsubcl  8723  qrevaddcl  8729  fseq1p1m1  9111  modqmuladdim  9369  frec2uzrand  9407  frecuzrdglem  9413  frecuzrdg0  9416  iseqfeq  9451  iseqdistr  9470  serige0  9473  serile  9474  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  zesq  9591  bcm1k  9687  bccl  9694  permnn  9698  shftuz  9705  ref  9742  imf  9743  crre  9744  rereb  9750  resqrexlemnm  9904  absf  9996  iserile  10180  oexpneg  10276  nn0ob  10308  divalglemqt  10319  gcdf  10364  lcmgcdlem  10459  sqnprm  10517  sqrt2irrlem  10540  2sqpwodd  10554