Theorem eleqtrrid 2867

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

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

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 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  rabsnt  4692  onnev  6486  opabiota  6960  canth  7367  onnseq  8333  tfrlem16  8382  oen0  8574  nnawordex  8625  inf0  9600  cantnflt  9651  cnfcom2  9681  cnfcom3lem  9682  cnfcom3  9683  r1ordg  9760  r1val1  9768  rankr1id  9844  acacni  10143  dfacacn  10144  dfac13  10145  ttukeylem5  10515  ttukeylem6  10516  gch2  10684  gch3  10685  gchac  10690  gchina  10708  swrds1  14736  wrdl3s3  15035  sadcp1  16545  lcmfunsnlem2  16730  fnpr2ob  17644  idfucl  17970  gsumval2  18788  gsumz  18945  frmdmnd  18968  frmd0  18969  efginvrel2  19854  efgcpbl2  19884  pgpfaclem1  20210  lbsexg  21351  zringndrg  21681  frlmlbs  22010  mat0dimscm  22691  mat0scmat  22760  m2detleiblem5  22847  m2detleiblem6  22848  m2detleiblem3  22851  m2detleiblem4  22852  d0mat2pmat  22963  chpmat0d  23059  dfac14  23844  acufl  24143  cnextfvval  24291  cnextcn  24293  minveclem3b  25656  minveclem4a  25658  ovollb2  25717  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliun2  25734  ioombl1lem4  25789  uniioombllem1  25809  uniioombllem2  25811  uniioombllem6  25816  itg2monolem1  25978  itg2mono  25981  itg2cnlem1  25989  xrlimcnp  27205  efrlim  27206  eengbas  29438  ebtwntg  29439  ecgrtg  29440  elntg  29441  wlkl1loop  30097  elwwlks2ons3im  30422  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  2clwwlk2clwwlk  30830  ex-br  30911  trsp2cyc  33563  cyc3evpm  33590  dflring3  33907  ply1dg1rtn0  33991  lvecdim0  34117  extdg1id  34176  irngss  34197  rge0scvg  34459  repr0  35119  hgt750lemg  35162  r1wf  35603  onvfowev  35713  mrsub0  36095  elmrsubrn  36099  topjoin  36984  finorwe  38136  pclfinN  40773  aomclem1  43895  dfac21  43907  naddgeoa  44235  clsk1indlem1  44885  mnurndlem1  45105  fourierdlem102  47036  fourierdlem114  47048  cycl3grtri  48863  lincval0  49345  lcoel0  49358  discsubc  49990  prsthinc  50390  isinito2lem  50424  termcarweu  50454  diag1f1o  50460  diag2f1o  50463  initocmd  50595