Theorem eleqtrrid 2844

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  rabsnt  4690  onnev  6453  opabiota  6924  canth  7322  onnseq  8286  tfrlem16  8334  oen0  8524  nnawordex  8575  inf0  9542  cantnflt  9593  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  r1ordg  9702  r1val1  9710  rankr1id  9786  acacni  10063  dfacacn  10064  dfac13  10065  ttukeylem5  10435  ttukeylem6  10436  gch2  10598  gch3  10599  gchac  10604  gchina  10622  swrds1  14602  wrdl3s3  14897  sadcp1  16394  lcmfunsnlem2  16579  fnpr2ob  17491  idfucl  17817  gsumval2  18623  gsumz  18773  frmdmnd  18796  frmd0  18797  efginvrel2  19668  efgcpbl2  19698  pgpfaclem1  20024  lbsexg  21131  zringndrg  21435  frlmlbs  21764  mat0dimscm  22425  mat0scmat  22494  m2detleiblem5  22581  m2detleiblem6  22582  m2detleiblem3  22585  m2detleiblem4  22586  d0mat2pmat  22694  chpmat0d  22790  dfac14  23574  acufl  23873  cnextfvval  24021  cnextcn  24023  minveclem3b  25396  minveclem4a  25398  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun2  25475  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem2  25552  uniioombllem6  25557  itg2monolem1  25719  itg2mono  25722  itg2cnlem1  25730  xrlimcnp  26946  efrlim  26947  efrlimOLD  26948  eengbas  29066  ebtwntg  29067  ecgrtg  29068  elntg  29069  wlkl1loop  29723  elwwlks2ons3im  30039  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  2clwwlk2clwwlk  30437  ex-br  30518  trsp2cyc  33217  cyc3evpm  33244  ply1dg1rtn0  33674  lvecdim0  33784  extdg1id  33844  irngss  33865  rge0scvg  34127  repr0  34789  hgt750lemg  34832  r1wf  35273  mrsub0  35732  elmrsubrn  35736  topjoin  36581  finorwe  37637  pclfinN  40276  aomclem1  43411  dfac21  43423  naddgeoa  43751  clsk1indlem1  44401  mnurndlem1  44637  fourierdlem102  46566  fourierdlem114  46578  cycl3grtri  48307  lincval0  48775  lcoel0  48788  discsubc  49423  prsthinc  49823  isinito2lem  49857  termcarweu  49887  diag1f1o  49893  diag2f1o  49896  initocmd  50028