Theorem eleqtrrid 2846

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 2744	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrid 2845	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  rabsnt  4664  onnev  6372  onnevOLD  6373  opabiota  6833  canth  7209  onnseq  8146  tfrlem16  8195  oen0  8379  nnawordex  8430  inf0  9309  cantnflt  9360  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  r1ordg  9467  r1val1  9475  rankr1id  9551  acacni  9827  dfacacn  9828  dfac13  9829  ttukeylem5  10200  ttukeylem6  10201  gch2  10362  gch3  10363  gchac  10368  gchina  10386  swrds1  14307  wrdl3s3  14605  sadcp1  16090  lcmfunsnlem2  16273  fnpr2ob  17186  idfucl  17512  gsumval2  18285  gsumz  18389  frmdmnd  18413  frmd0  18414  efginvrel2  19248  efgcpbl2  19278  pgpfaclem1  19599  lbsexg  20341  zringndrg  20602  frlmlbs  20914  mat0dimscm  21526  mat0scmat  21595  m2detleiblem5  21682  m2detleiblem6  21683  m2detleiblem3  21686  m2detleiblem4  21687  d0mat2pmat  21795  chpmat0d  21891  dfac14  22677  acufl  22976  cnextfvval  23124  cnextcn  23126  minveclem3b  24497  minveclem4a  24499  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliun2  24575  ioombl1lem4  24630  uniioombllem1  24650  uniioombllem2  24652  uniioombllem6  24657  itg2monolem1  24820  itg2mono  24823  itg2cnlem1  24831  xrlimcnp  26023  efrlim  26024  eengbas  27252  ebtwntg  27253  ecgrtg  27254  elntg  27255  wlkl1loop  27907  elwwlks2ons3im  28220  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  2clwwlk2clwwlk  28615  ex-br  28696  trsp2cyc  31292  cyc3evpm  31319  lvecdim0  31592  extdg1id  31640  rge0scvg  31801  repr0  32491  hgt750lemg  32534  mrsub0  33378  elmrsubrn  33382  topjoin  34481  finorwe  35480  pclfinN  37841  aomclem1  40795  dfac21  40807  clsk1indlem1  41544  mnurndlem1  41788  fourierdlem102  43639  fourierdlem114  43651  lincval0  45644  lcoel0  45657  prsthinc  46223