Theorem eleqtrrid 2897

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
eleqtrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrid

Step	Hyp	Ref	Expression
1		eleqtrrid.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2804	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrid 2896	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  rabsnt  4627  onnev  6279  onnevOLD  6280  opabiota  6721  canth  7090  onnseq  7964  tfrlem16  8012  oen0  8195  nnawordex  8246  inf0  9068  cantnflt  9119  cnfcom2  9149  cnfcom3lem  9150  cnfcom3  9151  r1ordg  9191  r1val1  9199  rankr1id  9275  acacni  9551  dfacacn  9552  dfac13  9553  ttukeylem5  9924  ttukeylem6  9925  gch2  10086  gch3  10087  gchac  10092  gchina  10110  swrds1  14019  wrdl3s3  14317  sadcp1  15794  lcmfunsnlem2  15974  fnpr2ob  16823  idfucl  17143  gsumval2  17888  gsumz  17992  frmdmnd  18016  frmd0  18017  efginvrel2  18845  efgcpbl2  18875  pgpfaclem1  19196  lbsexg  19929  zringndrg  20183  frlmlbs  20486  mat0dimscm  21074  mat0scmat  21143  m2detleiblem5  21230  m2detleiblem6  21231  m2detleiblem3  21234  m2detleiblem4  21235  d0mat2pmat  21343  chpmat0d  21439  dfac14  22223  acufl  22522  cnextfvval  22670  cnextcn  22672  minveclem3b  24032  minveclem4a  24034  ovollb2  24093  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliun2  24110  ioombl1lem4  24165  uniioombllem1  24185  uniioombllem2  24187  uniioombllem6  24192  itg2monolem1  24354  itg2mono  24357  itg2cnlem1  24365  xrlimcnp  25554  efrlim  25555  eengbas  26775  ebtwntg  26776  ecgrtg  26777  elntg  26778  wlkl1loop  27427  elwwlks2ons3im  27740  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  2clwwlk2clwwlk  28135  ex-br  28216  trsp2cyc  30815  cyc3evpm  30842  lvecdim0  31093  extdg1id  31141  rge0scvg  31302  repr0  31992  hgt750lemg  32035  mrsub0  32876  elmrsubrn  32880  topjoin  33826  finorwe  34799  pclfinN  37196  aomclem1  39998  dfac21  40010  clsk1indlem1  40748  mnurndlem1  40989  fourierdlem102  42850  fourierdlem114  42862  lincval0  44824  lcoel0  44837