Theorem eleqtrrd 2273

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

Hypotheses

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

Assertion

Ref	Expression
eleqtrrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2199	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2272	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  3eltr4d  2277  rspc2vd  3150  exmidsssnc  4233  tfrexlem  6389  nnsucuniel  6550  erref  6609  en1uniel  6860  fin0  6943  fin0or  6944  prarloclemarch2  7481  fzopth  10130  fzoss2  10242  fzosubel3  10266  elfzomin  10276  elfzonlteqm1  10280  fzoend  10292  fzofzp1  10297  fzofzp1b  10298  peano2fzor  10302  zmodfzo  10421  frecuzrdg0  10487  frecuzrdgsuc  10488  frecuzrdgdomlem  10491  frecuzrdg0t  10496  frecuzrdgsuctlem  10497  seq3f1olemqsum  10587  seqf1oglem2  10594  bcn2  10838  summodclem2a  11527  fisumss  11538  fsumm1  11562  fisumcom2  11584  prodmodclem2a  11722  fprodm1  11744  fprodcom2fi  11772  ennnfonelemex  12574  ctinfomlemom  12587  gsumpropd2  12979  sgrppropd  12999  mndpropd  13024  grpsubpropd2  13180  imasgrp  13184  subg0  13253  issubg2m  13262  ghmrn  13330  0ghm  13331  resghm2  13334  ghmco  13337  rngpropd  13454  imasrng  13455  srgpcomp  13489  srgpcompp  13490  srgpcomppsc  13491  ringpropd  13537  imasring  13563  qusring2  13565  mulgass3  13584  rhmopp  13675  lringuplu  13695  aprcotr  13784  lmodprop2d  13847  islssmd  13858  2idl0  14011  2idl1  14012  qus2idrng  14024  qus1  14025  qusrhm  14027  znf1o  14150  psrbaglesuppg  14169  lmtopcnp  14429  txopn  14444  blpnfctr  14618  metcnpi  14694  metcnpi2  14695  cncfmpt2fcntop  14778  limcimolemlt  14843  cnplimclemr  14848  limccnp2lem  14855  limccnp2cntop  14856  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvcn  14879  dvaddxxbr  14880  dvmulxxbr  14881  dvef  14906  lgseisenlem3  15229  lgseisenlem4  15230