Theorem eleqtrrid 2840

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  rabsnt  4735  onnev  6491  onnevOLD  6492  opabiota  6974  canth  7364  onnseq  8346  tfrlem16  8395  oen0  8588  nnawordex  8639  inf0  9618  cantnflt  9669  cnfcom2  9699  cnfcom3lem  9700  cnfcom3  9701  r1ordg  9775  r1val1  9783  rankr1id  9859  acacni  10137  dfacacn  10138  dfac13  10139  ttukeylem5  10510  ttukeylem6  10511  gch2  10672  gch3  10673  gchac  10678  gchina  10696  swrds1  14618  wrdl3s3  14915  sadcp1  16398  lcmfunsnlem2  16579  fnpr2ob  17506  idfucl  17833  gsumval2  18607  gsumz  18719  frmdmnd  18742  frmd0  18743  efginvrel2  19597  efgcpbl2  19627  pgpfaclem1  19953  lbsexg  20783  zringndrg  21044  frlmlbs  21358  mat0dimscm  21978  mat0scmat  22047  m2detleiblem5  22134  m2detleiblem6  22135  m2detleiblem3  22138  m2detleiblem4  22139  d0mat2pmat  22247  chpmat0d  22343  dfac14  23129  acufl  23428  cnextfvval  23576  cnextcn  23578  minveclem3b  24952  minveclem4a  24954  ovollb2  25013  ovolunlem1a  25020  ovolunlem1  25021  ovoliunlem1  25026  ovoliun2  25030  ioombl1lem4  25085  uniioombllem1  25105  uniioombllem2  25107  uniioombllem6  25112  itg2monolem1  25275  itg2mono  25278  itg2cnlem1  25286  xrlimcnp  26480  efrlim  26481  eengbas  28277  ebtwntg  28278  ecgrtg  28279  elntg  28280  wlkl1loop  28933  elwwlks2ons3im  29246  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  2clwwlk2clwwlk  29641  ex-br  29722  trsp2cyc  32323  cyc3evpm  32350  lvecdim0  32750  extdg1id  32801  irngss  32811  rge0scvg  32998  repr0  33692  hgt750lemg  33735  mrsub0  34576  elmrsubrn  34580  topjoin  35336  finorwe  36349  pclfinN  38857  aomclem1  41878  dfac21  41890  naddgeoa  42227  clsk1indlem1  42878  mnurndlem1  43122  fourierdlem102  45003  fourierdlem114  45015  lincval0  47174  lcoel0  47187  prsthinc  47752