Theorem eleqtrrid 2844

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  rabsnt  4676  onnev  6446  opabiota  6917  canth  7315  onnseq  8278  tfrlem16  8326  oen0  8516  nnawordex  8567  inf0  9536  cantnflt  9587  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  r1ordg  9696  r1val1  9704  rankr1id  9780  acacni  10057  dfacacn  10058  dfac13  10059  ttukeylem5  10429  ttukeylem6  10430  gch2  10592  gch3  10593  gchac  10598  gchina  10616  swrds1  14623  wrdl3s3  14918  sadcp1  16418  lcmfunsnlem2  16603  fnpr2ob  17516  idfucl  17842  gsumval2  18648  gsumz  18798  frmdmnd  18821  frmd0  18822  efginvrel2  19696  efgcpbl2  19726  pgpfaclem1  20052  lbsexg  21157  zringndrg  21461  frlmlbs  21790  mat0dimscm  22447  mat0scmat  22516  m2detleiblem5  22603  m2detleiblem6  22604  m2detleiblem3  22607  m2detleiblem4  22608  d0mat2pmat  22716  chpmat0d  22812  dfac14  23596  acufl  23895  cnextfvval  24043  cnextcn  24045  minveclem3b  25408  minveclem4a  25410  ovollb2  25469  ovolunlem1a  25476  ovolunlem1  25477  ovoliunlem1  25482  ovoliun2  25486  ioombl1lem4  25541  uniioombllem1  25561  uniioombllem2  25563  uniioombllem6  25568  itg2monolem1  25730  itg2mono  25733  itg2cnlem1  25741  xrlimcnp  26948  efrlim  26949  efrlimOLD  26950  eengbas  29067  ebtwntg  29068  ecgrtg  29069  elntg  29070  wlkl1loop  29724  elwwlks2ons3im  30040  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  2clwwlk2clwwlk  30438  ex-br  30519  trsp2cyc  33202  cyc3evpm  33229  ply1dg1rtn0  33659  lvecdim0  33769  extdg1id  33829  irngss  33850  rge0scvg  34112  repr0  34774  hgt750lemg  34817  r1wf  35258  mrsub0  35717  elmrsubrn  35721  topjoin  36566  finorwe  37715  pclfinN  40363  aomclem1  43503  dfac21  43515  naddgeoa  43843  clsk1indlem1  44493  mnurndlem1  44729  fourierdlem102  46657  fourierdlem114  46669  cycl3grtri  48438  lincval0  48906  lcoel0  48919  discsubc  49554  prsthinc  49954  isinito2lem  49988  termcarweu  50018  diag1f1o  50024  diag2f1o  50027  initocmd  50159