Theorem eleqtrrid 2841

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 2840	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  rabsnt  4686  onnev  6443  opabiota  6914  canth  7310  onnseq  8274  tfrlem16  8322  oen0  8512  nnawordex  8563  inf0  9528  cantnflt  9579  cnfcom2  9609  cnfcom3lem  9610  cnfcom3  9611  r1ordg  9688  r1val1  9696  rankr1id  9772  acacni  10049  dfacacn  10050  dfac13  10051  ttukeylem5  10421  ttukeylem6  10422  gch2  10584  gch3  10585  gchac  10590  gchina  10608  swrds1  14588  wrdl3s3  14883  sadcp1  16380  lcmfunsnlem2  16565  fnpr2ob  17477  idfucl  17803  gsumval2  18609  gsumz  18759  frmdmnd  18782  frmd0  18783  efginvrel2  19654  efgcpbl2  19684  pgpfaclem1  20010  lbsexg  21117  zringndrg  21421  frlmlbs  21750  mat0dimscm  22411  mat0scmat  22480  m2detleiblem5  22567  m2detleiblem6  22568  m2detleiblem3  22571  m2detleiblem4  22572  d0mat2pmat  22680  chpmat0d  22776  dfac14  23560  acufl  23859  cnextfvval  24007  cnextcn  24009  minveclem3b  25382  minveclem4a  25384  ovollb2  25444  ovolunlem1a  25451  ovolunlem1  25452  ovoliunlem1  25457  ovoliun2  25461  ioombl1lem4  25516  uniioombllem1  25536  uniioombllem2  25538  uniioombllem6  25543  itg2monolem1  25705  itg2mono  25708  itg2cnlem1  25716  xrlimcnp  26932  efrlim  26933  efrlimOLD  26934  eengbas  29003  ebtwntg  29004  ecgrtg  29005  elntg  29006  wlkl1loop  29660  elwwlks2ons3im  29976  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  2clwwlk2clwwlk  30374  ex-br  30455  trsp2cyc  33154  cyc3evpm  33181  ply1dg1rtn0  33611  lvecdim0  33712  extdg1id  33772  irngss  33793  rge0scvg  34055  repr0  34717  hgt750lemg  34760  r1wf  35201  mrsub0  35659  elmrsubrn  35663  topjoin  36508  finorwe  37526  pclfinN  40099  aomclem1  43238  dfac21  43250  naddgeoa  43578  clsk1indlem1  44228  mnurndlem1  44464  fourierdlem102  46394  fourierdlem114  46406  cycl3grtri  48135  lincval0  48603  lcoel0  48616  discsubc  49251  prsthinc  49651  isinito2lem  49685  termcarweu  49715  diag1f1o  49721  diag2f1o  49724  initocmd  49856