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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  rabsnt  4736  onnev  6492  onnevOLD  6493  opabiota  6975  canth  7362  onnseq  8344  tfrlem16  8393  oen0  8586  nnawordex  8637  inf0  9616  cantnflt  9667  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  r1ordg  9773  r1val1  9781  rankr1id  9857  acacni  10135  dfacacn  10136  dfac13  10137  ttukeylem5  10508  ttukeylem6  10509  gch2  10670  gch3  10671  gchac  10676  gchina  10694  swrds1  14616  wrdl3s3  14913  sadcp1  16396  lcmfunsnlem2  16577  fnpr2ob  17504  idfucl  17831  gsumval2  18605  gsumz  18717  frmdmnd  18740  frmd0  18741  efginvrel2  19595  efgcpbl2  19625  pgpfaclem1  19951  lbsexg  20777  zringndrg  21038  frlmlbs  21352  mat0dimscm  21971  mat0scmat  22040  m2detleiblem5  22127  m2detleiblem6  22128  m2detleiblem3  22131  m2detleiblem4  22132  d0mat2pmat  22240  chpmat0d  22336  dfac14  23122  acufl  23421  cnextfvval  23569  cnextcn  23571  minveclem3b  24945  minveclem4a  24947  ovollb2  25006  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliun2  25023  ioombl1lem4  25078  uniioombllem1  25098  uniioombllem2  25100  uniioombllem6  25105  itg2monolem1  25268  itg2mono  25271  itg2cnlem1  25279  xrlimcnp  26473  efrlim  26474  eengbas  28239  ebtwntg  28240  ecgrtg  28241  elntg  28242  wlkl1loop  28895  elwwlks2ons3im  29208  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  2clwwlk2clwwlk  29603  ex-br  29684  trsp2cyc  32282  cyc3evpm  32309  lvecdim0  32691  extdg1id  32742  irngss  32751  rge0scvg  32929  repr0  33623  hgt750lemg  33666  mrsub0  34507  elmrsubrn  34511  topjoin  35250  finorwe  36263  pclfinN  38771  aomclem1  41796  dfac21  41808  naddgeoa  42145  clsk1indlem1  42796  mnurndlem1  43040  fourierdlem102  44924  fourierdlem114  44936  lincval0  47096  lcoel0  47109  prsthinc  47674