Theorem eleqtrrid 2872

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  rabsnt  4699  onnev  6493  opabiota  6967  canth  7373  onnseq  8337  tfrlem16  8386  oen0  8578  nnawordex  8629  inf0  9597  cantnflt  9648  cnfcom2  9678  cnfcom3lem  9679  cnfcom3  9680  r1ordg  9757  r1val1  9765  rankr1id  9841  acacni  10140  dfacacn  10141  dfac13  10142  ttukeylem5  10512  ttukeylem6  10513  gch2  10675  gch3  10676  gchac  10681  gchina  10699  swrds1  14726  wrdl3s3  15023  sadcp1  16535  lcmfunsnlem2  16720  fnpr2ob  17634  idfucl  17960  gsumval2  18776  gsumz  18932  frmdmnd  18955  frmd0  18956  efginvrel2  19841  efgcpbl2  19871  pgpfaclem1  20197  lbsexg  21338  zringndrg  21668  frlmlbs  21997  mat0dimscm  22676  mat0scmat  22745  m2detleiblem5  22832  m2detleiblem6  22833  m2detleiblem3  22836  m2detleiblem4  22837  d0mat2pmat  22945  chpmat0d  23041  dfac14  23826  acufl  24125  cnextfvval  24273  cnextcn  24275  minveclem3b  25638  minveclem4a  25640  ovollb2  25699  ovolunlem1a  25706  ovolunlem1  25707  ovoliunlem1  25712  ovoliun2  25716  ioombl1lem4  25771  uniioombllem1  25791  uniioombllem2  25793  uniioombllem6  25798  itg2monolem1  25960  itg2mono  25963  itg2cnlem1  25971  xrlimcnp  27184  efrlim  27185  eengbas  29386  ebtwntg  29387  ecgrtg  29388  elntg  29389  wlkl1loop  30045  elwwlks2ons3im  30370  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  2clwwlk2clwwlk  30772  ex-br  30853  trsp2cyc  33507  cyc3evpm  33534  dflring3  33851  ply1dg1rtn0  33935  lvecdim0  34061  extdg1id  34120  irngss  34141  rge0scvg  34403  repr0  35063  hgt750lemg  35106  r1wf  35547  onvfowev  35657  mrsub0  36045  elmrsubrn  36049  topjoin  36933  finorwe  38085  pclfinN  40732  aomclem1  43839  dfac21  43851  naddgeoa  44179  clsk1indlem1  44829  mnurndlem1  45049  fourierdlem102  46980  fourierdlem114  46992  cycl3grtri  48770  lincval0  49252  lcoel0  49265  discsubc  49899  prsthinc  50299  isinito2lem  50333  termcarweu  50363  diag1f1o  50369  diag2f1o  50372  initocmd  50504