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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  rabsnt  4663  onnev  6438  opabiota  6909  canth  7310  onnseq  8274  tfrlem16  8322  oen0  8512  nnawordex  8563  inf0  9533  cantnflt  9584  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  r1ordg  9693  r1val1  9701  rankr1id  9777  acacni  10054  dfacacn  10055  dfac13  10056  ttukeylem5  10426  ttukeylem6  10427  gch2  10589  gch3  10590  gchac  10595  gchina  10613  swrds1  14620  wrdl3s3  14915  sadcp1  16415  lcmfunsnlem2  16600  fnpr2ob  17513  idfucl  17839  gsumval2  18645  gsumz  18795  frmdmnd  18818  frmd0  18819  efginvrel2  19693  efgcpbl2  19723  pgpfaclem1  20049  lbsexg  21157  zringndrg  21443  frlmlbs  21772  mat0dimscm  22452  mat0scmat  22521  m2detleiblem5  22608  m2detleiblem6  22609  m2detleiblem3  22612  m2detleiblem4  22613  d0mat2pmat  22721  chpmat0d  22817  dfac14  23601  acufl  23900  cnextfvval  24048  cnextcn  24050  minveclem3b  25413  minveclem4a  25415  ovollb2  25474  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliun2  25491  ioombl1lem4  25546  uniioombllem1  25566  uniioombllem2  25568  uniioombllem6  25573  itg2monolem1  25735  itg2mono  25738  itg2cnlem1  25746  xrlimcnp  26950  efrlim  26951  eengbas  29068  ebtwntg  29069  ecgrtg  29070  elntg  29071  wlkl1loop  29724  elwwlks2ons3im  30040  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  2clwwlk2clwwlk  30438  ex-br  30519  trsp2cyc  33204  cyc3evpm  33231  ply1dg1rtn0  33664  lvecdim0  33791  extdg1id  33850  irngss  33871  rge0scvg  34133  repr0  34795  hgt750lemg  34838  r1wf  35277  mrsub0  35744  elmrsubrn  35748  topjoin  36593  finorwe  37744  pclfinN  40392  aomclem1  43499  dfac21  43511  naddgeoa  43839  clsk1indlem1  44489  mnurndlem1  44725  fourierdlem102  46651  fourierdlem114  46663  cycl3grtri  48438  lincval0  48906  lcoel0  48919  discsubc  49554  prsthinc  49954  isinito2lem  49988  termcarweu  50018  diag1f1o  50024  diag2f1o  50027  initocmd  50159