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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  rabsnt  4735  onnev  6489  onnevOLD  6490  opabiota  6972  canth  7359  onnseq  8341  tfrlem16  8390  oen0  8583  nnawordex  8634  inf0  9613  cantnflt  9664  cnfcom2  9694  cnfcom3lem  9695  cnfcom3  9696  r1ordg  9770  r1val1  9778  rankr1id  9854  acacni  10132  dfacacn  10133  dfac13  10134  ttukeylem5  10505  ttukeylem6  10506  gch2  10667  gch3  10668  gchac  10673  gchina  10691  swrds1  14613  wrdl3s3  14910  sadcp1  16393  lcmfunsnlem2  16574  fnpr2ob  17501  idfucl  17828  gsumval2  18602  gsumz  18714  frmdmnd  18737  frmd0  18738  efginvrel2  19590  efgcpbl2  19620  pgpfaclem1  19946  lbsexg  20770  zringndrg  21030  frlmlbs  21344  mat0dimscm  21963  mat0scmat  22032  m2detleiblem5  22119  m2detleiblem6  22120  m2detleiblem3  22123  m2detleiblem4  22124  d0mat2pmat  22232  chpmat0d  22328  dfac14  23114  acufl  23413  cnextfvval  23561  cnextcn  23563  minveclem3b  24937  minveclem4a  24939  ovollb2  24998  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliun2  25015  ioombl1lem4  25070  uniioombllem1  25090  uniioombllem2  25092  uniioombllem6  25097  itg2monolem1  25260  itg2mono  25263  itg2cnlem1  25271  xrlimcnp  26463  efrlim  26464  eengbas  28229  ebtwntg  28230  ecgrtg  28231  elntg  28232  wlkl1loop  28885  elwwlks2ons3im  29198  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  2clwwlk2clwwlk  29593  ex-br  29674  trsp2cyc  32270  cyc3evpm  32297  lvecdim0  32680  extdg1id  32731  irngss  32740  rge0scvg  32918  repr0  33612  hgt750lemg  33655  mrsub0  34496  elmrsubrn  34500  topjoin  35239  finorwe  36252  pclfinN  38760  aomclem1  41782  dfac21  41794  naddgeoa  42131  clsk1indlem1  42782  mnurndlem1  43026  fourierdlem102  44911  fourierdlem114  44923  lincval0  47050  lcoel0  47063  prsthinc  47628