Theorem eleqtrrid 2835

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabsnt  4683  onnev  6435  opabiota  6905  canth  7303  onnseq  8267  tfrlem16  8315  oen0  8504  nnawordex  8555  inf0  9517  cantnflt  9568  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  r1ordg  9674  r1val1  9682  rankr1id  9758  acacni  10035  dfacacn  10036  dfac13  10037  ttukeylem5  10407  ttukeylem6  10408  gch2  10569  gch3  10570  gchac  10575  gchina  10593  swrds1  14573  wrdl3s3  14869  sadcp1  16366  lcmfunsnlem2  16551  fnpr2ob  17462  idfucl  17788  gsumval2  18560  gsumz  18710  frmdmnd  18733  frmd0  18734  efginvrel2  19606  efgcpbl2  19636  pgpfaclem1  19962  lbsexg  21071  zringndrg  21375  frlmlbs  21704  mat0dimscm  22354  mat0scmat  22423  m2detleiblem5  22510  m2detleiblem6  22511  m2detleiblem3  22514  m2detleiblem4  22515  d0mat2pmat  22623  chpmat0d  22719  dfac14  23503  acufl  23802  cnextfvval  23950  cnextcn  23952  minveclem3b  25326  minveclem4a  25328  ovollb2  25388  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovoliun2  25405  ioombl1lem4  25460  uniioombllem1  25480  uniioombllem2  25482  uniioombllem6  25487  itg2monolem1  25649  itg2mono  25652  itg2cnlem1  25660  xrlimcnp  26876  efrlim  26877  efrlimOLD  26878  eengbas  28926  ebtwntg  28927  ecgrtg  28928  elntg  28929  wlkl1loop  29583  elwwlks2ons3im  29899  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  2clwwlk2clwwlk  30294  ex-br  30375  trsp2cyc  33065  cyc3evpm  33092  ply1dg1rtn0  33516  lvecdim0  33573  extdg1id  33633  irngss  33654  rge0scvg  33916  repr0  34579  hgt750lemg  34622  mrsub0  35489  elmrsubrn  35493  topjoin  36339  finorwe  37356  pclfinN  39879  aomclem1  43027  dfac21  43039  naddgeoa  43367  clsk1indlem1  44018  mnurndlem1  44254  fourierdlem102  46189  fourierdlem114  46201  cycl3grtri  47931  lincval0  48400  lcoel0  48413  discsubc  49049  prsthinc  49449  isinito2lem  49483  termcarweu  49513  diag1f1o  49519  diag2f1o  49522  initocmd  49654