Theorem eleqtrrid 2839

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  rabsnt  4736  onnev  6492  onnevOLD  6493  opabiota  6975  canth  7365  onnseq  8347  tfrlem16  8396  oen0  8589  nnawordex  8640  inf0  9619  cantnflt  9670  cnfcom2  9700  cnfcom3lem  9701  cnfcom3  9702  r1ordg  9776  r1val1  9784  rankr1id  9860  acacni  10138  dfacacn  10139  dfac13  10140  ttukeylem5  10511  ttukeylem6  10512  gch2  10673  gch3  10674  gchac  10679  gchina  10697  swrds1  14621  wrdl3s3  14918  sadcp1  16401  lcmfunsnlem2  16582  fnpr2ob  17509  idfucl  17836  gsumval2  18612  gsumz  18754  frmdmnd  18777  frmd0  18778  efginvrel2  19637  efgcpbl2  19667  pgpfaclem1  19993  lbsexg  20923  zringndrg  21240  frlmlbs  21572  mat0dimscm  22192  mat0scmat  22261  m2detleiblem5  22348  m2detleiblem6  22349  m2detleiblem3  22352  m2detleiblem4  22353  d0mat2pmat  22461  chpmat0d  22557  dfac14  23343  acufl  23642  cnextfvval  23790  cnextcn  23792  minveclem3b  25177  minveclem4a  25179  ovollb2  25239  ovolunlem1a  25246  ovolunlem1  25247  ovoliunlem1  25252  ovoliun2  25256  ioombl1lem4  25311  uniioombllem1  25331  uniioombllem2  25333  uniioombllem6  25338  itg2monolem1  25501  itg2mono  25504  itg2cnlem1  25512  xrlimcnp  26706  efrlim  26707  eengbas  28503  ebtwntg  28504  ecgrtg  28505  elntg  28506  wlkl1loop  29159  elwwlks2ons3im  29472  upgr3v3e3cycl  29697  upgr4cycl4dv4e  29702  2clwwlk2clwwlk  29867  ex-br  29948  trsp2cyc  32549  cyc3evpm  32576  lvecdim0  32976  extdg1id  33027  irngss  33037  rge0scvg  33224  repr0  33918  hgt750lemg  33961  mrsub0  34802  elmrsubrn  34806  topjoin  35554  finorwe  36567  pclfinN  39075  aomclem1  42099  dfac21  42111  naddgeoa  42448  clsk1indlem1  43099  mnurndlem1  43343  fourierdlem102  45224  fourierdlem114  45236  lincval0  47185  lcoel0  47198  prsthinc  47763