Theorem eleqtrrid 2876

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  rabsnt  4702  onnev  6490  opabiota  6964  canth  7365  onnseq  8330  tfrlem16  8379  oen0  8571  nnawordex  8622  inf0  9589  cantnflt  9640  cnfcom2  9670  cnfcom3lem  9671  cnfcom3  9672  r1ordg  9749  r1val1  9757  rankr1id  9833  acacni  10123  dfacacn  10124  dfac13  10125  ttukeylem5  10496  ttukeylem6  10497  gch2  10659  gch3  10660  gchac  10665  gchina  10683  swrds1  14703  wrdl3s3  14998  sadcp1  16512  lcmfunsnlem2  16697  fnpr2ob  17611  idfucl  17937  gsumval2  18743  gsumz  18894  frmdmnd  18917  frmd0  18918  efginvrel2  19796  efgcpbl2  19826  pgpfaclem1  20152  lbsexg  21265  zringndrg  21586  frlmlbs  21915  mat0dimscm  22594  mat0scmat  22663  m2detleiblem5  22750  m2detleiblem6  22751  m2detleiblem3  22754  m2detleiblem4  22755  d0mat2pmat  22863  chpmat0d  22959  dfac14  23743  acufl  24042  cnextfvval  24190  cnextcn  24192  minveclem3b  25555  minveclem4a  25557  ovollb2  25616  ovolunlem1a  25623  ovolunlem1  25624  ovoliunlem1  25629  ovoliun2  25633  ioombl1lem4  25688  uniioombllem1  25708  uniioombllem2  25710  uniioombllem6  25715  itg2monolem1  25877  itg2mono  25880  itg2cnlem1  25888  xrlimcnp  27098  efrlim  27099  eengbas  29271  ebtwntg  29272  ecgrtg  29273  elntg  29274  wlkl1loop  29927  elwwlks2ons3im  30243  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  2clwwlk2clwwlk  30641  ex-br  30722  trsp2cyc  33383  cyc3evpm  33410  dflring3  33731  ply1dg1rtn0  33815  lvecdim0  33941  extdg1id  34000  irngss  34021  rge0scvg  34283  repr0  34942  hgt750lemg  34985  r1wf  35431  onvfowev  35498  mrsub0  35906  elmrsubrn  35910  topjoin  36764  finorwe  37915  pclfinN  40563  aomclem1  43672  dfac21  43684  naddgeoa  44012  clsk1indlem1  44662  mnurndlem1  44882  fourierdlem102  46813  fourierdlem114  46825  cycl3grtri  48600  lincval0  49079  lcoel0  49092  discsubc  49726  prsthinc  50126  isinito2lem  50160  termcarweu  50190  diag1f1o  50196  diag2f1o  50199  initocmd  50331