Theorem eleqtrrid 2832

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-clel 2802

This theorem is referenced by:  rabsnt  4727  onnev  6481  onnevOLD  6482  opabiota  6964  canth  7354  onnseq  8339  tfrlem16  8388  oen0  8581  nnawordex  8632  inf0  9611  cantnflt  9662  cnfcom2  9692  cnfcom3lem  9693  cnfcom3  9694  r1ordg  9768  r1val1  9776  rankr1id  9852  acacni  10130  dfacacn  10131  dfac13  10132  ttukeylem5  10503  ttukeylem6  10504  gch2  10665  gch3  10666  gchac  10671  gchina  10689  swrds1  14612  wrdl3s3  14909  sadcp1  16392  lcmfunsnlem2  16573  fnpr2ob  17502  idfucl  17829  gsumval2  18608  gsumz  18750  frmdmnd  18773  frmd0  18774  efginvrel2  19636  efgcpbl2  19666  pgpfaclem1  19992  lbsexg  21004  zringndrg  21322  frlmlbs  21659  mat0dimscm  22292  mat0scmat  22361  m2detleiblem5  22448  m2detleiblem6  22449  m2detleiblem3  22452  m2detleiblem4  22453  d0mat2pmat  22561  chpmat0d  22657  dfac14  23443  acufl  23742  cnextfvval  23890  cnextcn  23892  minveclem3b  25277  minveclem4a  25279  ovollb2  25339  ovolunlem1a  25346  ovolunlem1  25347  ovoliunlem1  25352  ovoliun2  25356  ioombl1lem4  25411  uniioombllem1  25431  uniioombllem2  25433  uniioombllem6  25438  itg2monolem1  25601  itg2mono  25604  itg2cnlem1  25612  xrlimcnp  26815  efrlim  26816  efrlimOLD  26817  eengbas  28674  ebtwntg  28675  ecgrtg  28676  elntg  28677  wlkl1loop  29330  elwwlks2ons3im  29643  upgr3v3e3cycl  29868  upgr4cycl4dv4e  29873  2clwwlk2clwwlk  30038  ex-br  30119  trsp2cyc  32716  cyc3evpm  32743  lvecdim0  33136  extdg1id  33187  irngss  33197  rge0scvg  33384  repr0  34078  hgt750lemg  34121  mrsub0  34962  elmrsubrn  34966  topjoin  35706  finorwe  36719  pclfinN  39227  aomclem1  42251  dfac21  42263  naddgeoa  42600  clsk1indlem1  43251  mnurndlem1  43495  fourierdlem102  45375  fourierdlem114  45387  lincval0  47250  lcoel0  47263  prsthinc  47828