Theorem eleqtrrid 2869

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  rabsnt  4690  onnev  6474  opabiota  6949  canth  7350  onnseq  8315  tfrlem16  8364  oen0  8556  nnawordex  8607  inf0  9576  cantnflt  9627  cnfcom2  9657  cnfcom3lem  9658  cnfcom3  9659  r1ordg  9736  r1val1  9744  rankr1id  9820  acacni  10097  dfacacn  10098  dfac13  10099  ttukeylem5  10470  ttukeylem6  10471  gch2  10633  gch3  10634  gchac  10639  gchina  10657  swrds1  14680  wrdl3s3  14975  sadcp1  16489  lcmfunsnlem2  16674  fnpr2ob  17588  idfucl  17914  gsumval2  18720  gsumz  18870  frmdmnd  18893  frmd0  18894  efginvrel2  19767  efgcpbl2  19797  pgpfaclem1  20123  lbsexg  21231  zringndrg  21517  frlmlbs  21846  mat0dimscm  22526  mat0scmat  22595  m2detleiblem5  22682  m2detleiblem6  22683  m2detleiblem3  22686  m2detleiblem4  22687  d0mat2pmat  22795  chpmat0d  22891  dfac14  23675  acufl  23974  cnextfvval  24122  cnextcn  24124  minveclem3b  25487  minveclem4a  25489  ovollb2  25548  ovolunlem1a  25555  ovolunlem1  25556  ovoliunlem1  25561  ovoliun2  25565  ioombl1lem4  25620  uniioombllem1  25640  uniioombllem2  25642  uniioombllem6  25647  itg2monolem1  25809  itg2mono  25812  itg2cnlem1  25820  xrlimcnp  27030  efrlim  27031  eengbas  29179  ebtwntg  29180  ecgrtg  29181  elntg  29182  wlkl1loop  29835  elwwlks2ons3im  30151  upgr3v3e3cycl  30379  upgr4cycl4dv4e  30384  2clwwlk2clwwlk  30549  ex-br  30630  trsp2cyc  33300  cyc3evpm  33327  dflring3  33690  ply1dg1rtn0  33774  lvecdim0  33901  extdg1id  33960  irngss  33981  rge0scvg  34243  repr0  34902  hgt750lemg  34945  r1wf  35389  onvfowev  35456  mrsub0  35863  elmrsubrn  35867  topjoin  36722  finorwe  37873  pclfinN  40521  aomclem1  43628  dfac21  43640  naddgeoa  43968  clsk1indlem1  44618  mnurndlem1  44854  fourierdlem102  46779  fourierdlem114  46791  cycl3grtri  48566  lincval0  49034  lcoel0  49047  discsubc  49682  prsthinc  50082  isinito2lem  50116  termcarweu  50146  diag1f1o  50152  diag2f1o  50155  initocmd  50287