Theorem eqeltrrd 2115

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 2045	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2114	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  3eltr3d  2120  xpexr2m  4762  funimaexg  4983  fvmptdv2  5260  ffvresb  5328  2ndrn  5809  1st2ndbr  5810  elopabi  5821  cnvf1olem  5845  dftpos4  5878  tfrlemibxssdm  5941  nnmordi  6089  th3qlem1  6208  onunsnss  6355  ordiso2  6357  archnqq  6515  prarloclemarch2  6517  enq0tr  6532  nqnq0  6539  addcmpblnq0  6541  mulcmpblnq0  6542  mulcanenq0ec  6543  addclnq0  6549  mulclnq0  6550  nqpnq0nq  6551  nq0m0r  6554  distrnq0  6557  addassnq0lemcl  6559  prarloclemlt  6591  prarloclem5  6598  distrlem4prl  6682  distrlem4pru  6683  ltexprlemm  6698  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  cauappcvgprlemladdru  6754  prsrlem1  6827  mulgt0sr  6862  cnegexlem2  7187  subf  7213  resubcl  7275  negcon1ad  7317  subeq0bd  7377  rimul  7576  rereim  7577  nn0nnaddcl  8213  elnn0nn  8224  zaddcllemneg  8284  zsubcl  8286  zrevaddcl  8295  elz2  8312  zdiv  8328  peano5uzti  8346  peano2uzr  8528  uzaddcl  8529  divfnzn  8556  qsubcl  8573  qrevaddcl  8578  fseq1p1m1  8956  frec2uzrand  9191  frecuzrdglem  9197  frecuzrdg0  9200  iseqfeq  9231  iseqdistr  9249  serige0  9252  serile  9253  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  zesq  9367  shftuz  9418  ref  9455  imf  9456  crre  9457  rereb  9463  resqrexlemnm  9616  absf  9706  iserile  9862  sqr2irrlem  9877