Theorem eleqtrrid 2841

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  rabsnt  4707  onnev  6480  opabiota  6960  canth  7357  onnseq  8356  tfrlem16  8405  oen0  8596  nnawordex  8647  inf0  9633  cantnflt  9684  cnfcom2  9714  cnfcom3lem  9715  cnfcom3  9716  r1ordg  9790  r1val1  9798  rankr1id  9874  acacni  10153  dfacacn  10154  dfac13  10155  ttukeylem5  10525  ttukeylem6  10526  gch2  10687  gch3  10688  gchac  10693  gchina  10711  swrds1  14682  wrdl3s3  14979  sadcp1  16472  lcmfunsnlem2  16657  fnpr2ob  17570  idfucl  17892  gsumval2  18662  gsumz  18812  frmdmnd  18835  frmd0  18836  efginvrel2  19706  efgcpbl2  19736  pgpfaclem1  20062  lbsexg  21123  zringndrg  21427  frlmlbs  21755  mat0dimscm  22405  mat0scmat  22474  m2detleiblem5  22561  m2detleiblem6  22562  m2detleiblem3  22565  m2detleiblem4  22566  d0mat2pmat  22674  chpmat0d  22770  dfac14  23554  acufl  23853  cnextfvval  24001  cnextcn  24003  minveclem3b  25378  minveclem4a  25380  ovollb2  25440  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliun2  25457  ioombl1lem4  25512  uniioombllem1  25532  uniioombllem2  25534  uniioombllem6  25539  itg2monolem1  25701  itg2mono  25704  itg2cnlem1  25712  xrlimcnp  26928  efrlim  26929  efrlimOLD  26930  eengbas  28906  ebtwntg  28907  ecgrtg  28908  elntg  28909  wlkl1loop  29564  elwwlks2ons3im  29882  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  2clwwlk2clwwlk  30277  ex-br  30358  trsp2cyc  33080  cyc3evpm  33107  ply1dg1rtn0  33539  lvecdim0  33592  extdg1id  33653  irngss  33674  rge0scvg  33926  repr0  34589  hgt750lemg  34632  mrsub0  35484  elmrsubrn  35488  topjoin  36329  finorwe  37346  pclfinN  39865  aomclem1  43025  dfac21  43037  naddgeoa  43365  clsk1indlem1  44016  mnurndlem1  44253  fourierdlem102  46185  fourierdlem114  46197  cycl3grtri  47907  lincval0  48339  lcoel0  48352  discsubc  48979  prsthinc  49298  isinito2lem  49331  termcarweu  49361  diag1f1o  49367  diag2f1o  49370