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 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  rabsnt  4667  onnev  6387  onnevOLD  6388  opabiota  6851  canth  7229  onnseq  8175  tfrlem16  8224  oen0  8417  nnawordex  8468  inf0  9379  cantnflt  9430  cnfcom2  9460  cnfcom3lem  9461  cnfcom3  9462  r1ordg  9536  r1val1  9544  rankr1id  9620  acacni  9896  dfacacn  9897  dfac13  9898  ttukeylem5  10269  ttukeylem6  10270  gch2  10431  gch3  10432  gchac  10437  gchina  10455  swrds1  14379  wrdl3s3  14677  sadcp1  16162  lcmfunsnlem2  16345  fnpr2ob  17269  idfucl  17596  gsumval2  18370  gsumz  18474  frmdmnd  18498  frmd0  18499  efginvrel2  19333  efgcpbl2  19363  pgpfaclem1  19684  lbsexg  20426  zringndrg  20690  frlmlbs  21004  mat0dimscm  21618  mat0scmat  21687  m2detleiblem5  21774  m2detleiblem6  21775  m2detleiblem3  21778  m2detleiblem4  21779  d0mat2pmat  21887  chpmat0d  21983  dfac14  22769  acufl  23068  cnextfvval  23216  cnextcn  23218  minveclem3b  24592  minveclem4a  24594  ovollb2  24653  ovolunlem1a  24660  ovolunlem1  24661  ovoliunlem1  24666  ovoliun2  24670  ioombl1lem4  24725  uniioombllem1  24745  uniioombllem2  24747  uniioombllem6  24752  itg2monolem1  24915  itg2mono  24918  itg2cnlem1  24926  xrlimcnp  26118  efrlim  26119  eengbas  27349  ebtwntg  27350  ecgrtg  27351  elntg  27352  wlkl1loop  28005  elwwlks2ons3im  28319  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  2clwwlk2clwwlk  28714  ex-br  28795  trsp2cyc  31390  cyc3evpm  31417  lvecdim0  31690  extdg1id  31738  rge0scvg  31899  repr0  32591  hgt750lemg  32634  mrsub0  33478  elmrsubrn  33482  topjoin  34554  finorwe  35553  pclfinN  37914  aomclem1  40879  dfac21  40891  clsk1indlem1  41655  mnurndlem1  41899  fourierdlem102  43749  fourierdlem114  43761  lincval0  45756  lcoel0  45769  prsthinc  46335