Theorem eleqtrrid 2871

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  rabsnt  4694  onnev  6517  opabiota  6998  canth  7405  onnseq  8390  tfrlem16  8439  oen0  8633  nnawordex  8684  inf0  9659  cantnflt  9710  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  r1ordg  9822  r1val1  9830  r1wf  9878  rankr1id  9915  acacni  10258  dfacacn  10259  dfac13  10260  ttukeylem5  10630  ttukeylem6  10631  gch2  10799  gch3  10800  gchac  10805  gchina  10823  swrds1  14858  wrdl3s3  15158  sadcp1  16669  lcmfunsnlem2  16859  fnpr2ob  17780  idfucl  18106  gsumval2  18925  gsumz  19082  frmdmnd  19105  frmd0  19106  efginvrel2  19992  efgcpbl2  20022  pgpfaclem1  20348  lbsexg  21493  zringndrg  21829  frlmlbs  22158  mat0dimscm  22839  mat0scmat  22908  m2detleiblem5  22995  m2detleiblem6  22996  m2detleiblem3  22999  m2detleiblem4  23000  d0mat2pmat  23111  chpmat0d  23207  dfac14  23992  acufl  24291  cnextfvval  24439  cnextcn  24441  minveclem3b  25804  minveclem4a  25806  ovollb2  25865  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliun2  25882  ioombl1lem4  25937  uniioombllem1  25957  uniioombllem2  25959  uniioombllem6  25964  itg2monolem1  26126  itg2mono  26129  itg2cnlem1  26137  xrlimcnp  27353  efrlim  27354  eengbas  29616  ebtwntg  29617  ecgrtg  29618  elntg  29619  wlkl1loop  30275  elwwlks2ons3im  30600  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  2clwwlk2clwwlk  31008  ex-br  31089  trsp2cyc  33783  cyc3evpm  33810  dflring3  34133  ply1dg1rtn0  34216  lvecdim0  34350  extdg1id  34409  irngss  34430  rge0scvg  34692  repr0  35351  hgt750lemg  35394  onvfowev  36091  mrsub0  36489  elmrsubrn  36493  topjoin  37368  finorwe  38573  pclfinN  41223  aomclem1  44322  dfac21  44334  naddgeoa  44657  clsk1indlem1  45306  mnurndlem1  45526  fourierdlem102  47491  fourierdlem114  47503  cycl3grtri  49318  lincval0  49858  lcoel0  49871  discsubc  50509  prsthinc  50930  isinito2lem  50964  termcarweu  50994  diag1f1o  51000  diag2f1o  51006  parhomid2  51082  parhomid  51083  initocmd  51183