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  4691  onnev  6449  opabiota  6925  canth  7323  onnseq  8290  tfrlem16  8338  oen0  8527  nnawordex  8578  inf0  9550  cantnflt  9601  cnfcom2  9631  cnfcom3lem  9632  cnfcom3  9633  r1ordg  9707  r1val1  9715  rankr1id  9791  acacni  10070  dfacacn  10071  dfac13  10072  ttukeylem5  10442  ttukeylem6  10443  gch2  10604  gch3  10605  gchac  10610  gchina  10628  swrds1  14607  wrdl3s3  14904  sadcp1  16401  lcmfunsnlem2  16586  fnpr2ob  17497  idfucl  17819  gsumval2  18589  gsumz  18739  frmdmnd  18762  frmd0  18763  efginvrel2  19633  efgcpbl2  19663  pgpfaclem1  19989  lbsexg  21050  zringndrg  21354  frlmlbs  21682  mat0dimscm  22332  mat0scmat  22401  m2detleiblem5  22488  m2detleiblem6  22489  m2detleiblem3  22492  m2detleiblem4  22493  d0mat2pmat  22601  chpmat0d  22697  dfac14  23481  acufl  23780  cnextfvval  23928  cnextcn  23930  minveclem3b  25304  minveclem4a  25306  ovollb2  25366  ovolunlem1a  25373  ovolunlem1  25374  ovoliunlem1  25379  ovoliun2  25383  ioombl1lem4  25438  uniioombllem1  25458  uniioombllem2  25460  uniioombllem6  25465  itg2monolem1  25627  itg2mono  25630  itg2cnlem1  25638  xrlimcnp  26854  efrlim  26855  efrlimOLD  26856  eengbas  28884  ebtwntg  28885  ecgrtg  28886  elntg  28887  wlkl1loop  29541  elwwlks2ons3im  29857  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  2clwwlk2clwwlk  30252  ex-br  30333  trsp2cyc  33053  cyc3evpm  33080  ply1dg1rtn0  33522  lvecdim0  33575  extdg1id  33634  irngss  33655  rge0scvg  33912  repr0  34575  hgt750lemg  34618  mrsub0  35476  elmrsubrn  35480  topjoin  36326  finorwe  37343  pclfinN  39867  aomclem1  43016  dfac21  43028  naddgeoa  43356  clsk1indlem1  44007  mnurndlem1  44243  fourierdlem102  46179  fourierdlem114  46191  cycl3grtri  47919  lincval0  48377  lcoel0  48390  discsubc  49026  prsthinc  49426  isinito2lem  49460  termcarweu  49490  diag1f1o  49496  diag2f1o  49499  initocmd  49631