Theorem eleqtrrid 2920

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  rabsnt  4667  onnev  6311  opabiota  6746  canth  7111  onnseq  7981  tfrlem16  8029  oen0  8212  nnawordex  8263  inf0  9084  cantnflt  9135  cnfcom2  9165  cnfcom3lem  9166  cnfcom3  9167  r1ordg  9207  r1val1  9215  rankr1id  9291  acacni  9566  dfacacn  9567  dfac13  9568  ttukeylem5  9935  ttukeylem6  9936  gch2  10097  gch3  10098  gchac  10103  gchina  10121  swrds1  14028  wrdl3s3  14326  sadcp1  15804  lcmfunsnlem2  15984  fnpr2ob  16831  idfucl  17151  gsumval2  17896  gsumz  18000  frmdmnd  18024  frmd0  18025  efginvrel2  18853  efgcpbl2  18883  pgpfaclem1  19203  lbsexg  19936  zringndrg  20637  frlmlbs  20941  mat0dimscm  21078  mat0scmat  21147  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  d0mat2pmat  21346  chpmat0d  21442  dfac14  22226  acufl  22525  cnextfvval  22673  cnextcn  22675  minveclem3b  24031  minveclem4a  24033  ovollb2  24090  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliun2  24107  ioombl1lem4  24162  uniioombllem1  24182  uniioombllem2  24184  uniioombllem6  24189  itg2monolem1  24351  itg2mono  24354  itg2cnlem1  24362  xrlimcnp  25546  efrlim  25547  eengbas  26767  ebtwntg  26768  ecgrtg  26769  elntg  26770  wlkl1loop  27419  elwwlks2ons3im  27733  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  2clwwlk2clwwlk  28129  ex-br  28210  trsp2cyc  30765  cyc3evpm  30792  lvecdim0  31005  extdg1id  31053  rge0scvg  31192  repr0  31882  hgt750lemg  31925  mrsub0  32763  elmrsubrn  32767  topjoin  33713  finorwe  34666  pclfinN  37051  aomclem1  39703  dfac21  39715  clsk1indlem1  40444  mnurndlem1  40666  fourierdlem102  42542  fourierdlem114  42554  lincval0  44519  lcoel0  44532