Theorem eleqtrrid 2836

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  rabsnt  4698  onnev  6464  opabiota  6946  canth  7344  onnseq  8316  tfrlem16  8364  oen0  8553  nnawordex  8604  inf0  9581  cantnflt  9632  cnfcom2  9662  cnfcom3lem  9663  cnfcom3  9664  r1ordg  9738  r1val1  9746  rankr1id  9822  acacni  10101  dfacacn  10102  dfac13  10103  ttukeylem5  10473  ttukeylem6  10474  gch2  10635  gch3  10636  gchac  10641  gchina  10659  swrds1  14638  wrdl3s3  14935  sadcp1  16432  lcmfunsnlem2  16617  fnpr2ob  17528  idfucl  17850  gsumval2  18620  gsumz  18770  frmdmnd  18793  frmd0  18794  efginvrel2  19664  efgcpbl2  19694  pgpfaclem1  20020  lbsexg  21081  zringndrg  21385  frlmlbs  21713  mat0dimscm  22363  mat0scmat  22432  m2detleiblem5  22519  m2detleiblem6  22520  m2detleiblem3  22523  m2detleiblem4  22524  d0mat2pmat  22632  chpmat0d  22728  dfac14  23512  acufl  23811  cnextfvval  23959  cnextcn  23961  minveclem3b  25335  minveclem4a  25337  ovollb2  25397  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun2  25414  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem2  25491  uniioombllem6  25496  itg2monolem1  25658  itg2mono  25661  itg2cnlem1  25669  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  eengbas  28915  ebtwntg  28916  ecgrtg  28917  elntg  28918  wlkl1loop  29573  elwwlks2ons3im  29891  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  2clwwlk2clwwlk  30286  ex-br  30367  trsp2cyc  33087  cyc3evpm  33114  ply1dg1rtn0  33556  lvecdim0  33609  extdg1id  33668  irngss  33689  rge0scvg  33946  repr0  34609  hgt750lemg  34652  mrsub0  35510  elmrsubrn  35514  topjoin  36360  finorwe  37377  pclfinN  39901  aomclem1  43050  dfac21  43062  naddgeoa  43390  clsk1indlem1  44041  mnurndlem1  44277  fourierdlem102  46213  fourierdlem114  46225  cycl3grtri  47950  lincval0  48408  lcoel0  48421  discsubc  49057  prsthinc  49457  isinito2lem  49491  termcarweu  49521  diag1f1o  49527  diag2f1o  49530  initocmd  49662