Theorem eleqtrrid 2868

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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

This theorem is used by:  rabsnt  4692  onnev  6490  opabiota  6965  canth  7372  onnseq  8345  tfrlem16  8394  oen0  8588  nnawordex  8639  inf0  9615  cantnflt  9666  cnfcom2  9696  cnfcom3lem  9697  cnfcom3  9698  r1ordg  9778  r1val1  9786  r1wf  9834  rankr1id  9871  acacni  10212  dfacacn  10213  dfac13  10214  ttukeylem5  10584  ttukeylem6  10585  gch2  10753  gch3  10754  gchac  10759  gchina  10777  swrds1  14809  wrdl3s3  15108  sadcp1  16618  lcmfunsnlem2  16808  fnpr2ob  17723  idfucl  18049  gsumval2  18868  gsumz  19025  frmdmnd  19048  frmd0  19049  efginvrel2  19934  efgcpbl2  19964  pgpfaclem1  20290  lbsexg  21435  zringndrg  21767  frlmlbs  22096  mat0dimscm  22777  mat0scmat  22846  m2detleiblem5  22933  m2detleiblem6  22934  m2detleiblem3  22937  m2detleiblem4  22938  d0mat2pmat  23049  chpmat0d  23145  dfac14  23930  acufl  24229  cnextfvval  24377  cnextcn  24379  minveclem3b  25742  minveclem4a  25744  ovollb2  25803  ovolunlem1a  25810  ovolunlem1  25811  ovoliunlem1  25816  ovoliun2  25820  ioombl1lem4  25875  uniioombllem1  25895  uniioombllem2  25897  uniioombllem6  25902  itg2monolem1  26064  itg2mono  26067  itg2cnlem1  26075  xrlimcnp  27289  efrlim  27290  eengbas  29552  ebtwntg  29553  ecgrtg  29554  elntg  29555  wlkl1loop  30211  elwwlks2ons3im  30536  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  2clwwlk2clwwlk  30944  ex-br  31025  trsp2cyc  33677  cyc3evpm  33704  dflring3  34022  ply1dg1rtn0  34106  lvecdim0  34232  extdg1id  34291  irngss  34312  rge0scvg  34574  repr0  35233  hgt750lemg  35276  onvfowev  35878  mrsub0  36260  elmrsubrn  36264  topjoin  37133  finorwe  38285  pclfinN  40937  aomclem1  44040  dfac21  44052  naddgeoa  44380  clsk1indlem1  45030  mnurndlem1  45250  fourierdlem102  47187  fourierdlem114  47199  cycl3grtri  49014  lincval0  49496  lcoel0  49509  discsubc  50141  prsthinc  50541  isinito2lem  50575  termcarweu  50605  diag1f1o  50611  diag2f1o  50614  initocmd  50746