Theorem eleqtrrid 2845

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  rabsnt  4735  onnev  6512  opabiota  6990  canth  7384  onnseq  8382  tfrlem16  8431  oen0  8622  nnawordex  8673  inf0  9658  cantnflt  9709  cnfcom2  9739  cnfcom3lem  9740  cnfcom3  9741  r1ordg  9815  r1val1  9823  rankr1id  9899  acacni  10178  dfacacn  10179  dfac13  10180  ttukeylem5  10550  ttukeylem6  10551  gch2  10712  gch3  10713  gchac  10718  gchina  10736  swrds1  14700  wrdl3s3  14997  sadcp1  16488  lcmfunsnlem2  16673  fnpr2ob  17604  idfucl  17931  gsumval2  18711  gsumz  18861  frmdmnd  18884  frmd0  18885  efginvrel2  19759  efgcpbl2  19789  pgpfaclem1  20115  lbsexg  21183  zringndrg  21496  frlmlbs  21834  mat0dimscm  22490  mat0scmat  22559  m2detleiblem5  22646  m2detleiblem6  22647  m2detleiblem3  22650  m2detleiblem4  22651  d0mat2pmat  22759  chpmat0d  22855  dfac14  23641  acufl  23940  cnextfvval  24088  cnextcn  24090  minveclem3b  25475  minveclem4a  25477  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun2  25554  ioombl1lem4  25609  uniioombllem1  25629  uniioombllem2  25631  uniioombllem6  25636  itg2monolem1  25799  itg2mono  25802  itg2cnlem1  25810  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  eengbas  29010  ebtwntg  29011  ecgrtg  29012  elntg  29013  wlkl1loop  29670  elwwlks2ons3im  29983  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  2clwwlk2clwwlk  30378  ex-br  30459  trsp2cyc  33125  cyc3evpm  33152  ply1dg1rtn0  33584  lvecdim0  33633  extdg1id  33690  irngss  33701  rge0scvg  33909  repr0  34604  hgt750lemg  34647  mrsub0  35500  elmrsubrn  35504  topjoin  36347  finorwe  37364  pclfinN  39882  aomclem1  43042  dfac21  43054  naddgeoa  43383  clsk1indlem1  44034  mnurndlem1  44276  fourierdlem102  46163  fourierdlem114  46175  lincval0  48260  lcoel0  48273  prsthinc  48854