Theorem eleqtrrid 2843

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 2742	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrid 2842	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 2708

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

This theorem is referenced by:  rabsnt  4675  onnev  6451  opabiota  6922  canth  7321  onnseq  8284  tfrlem16  8332  oen0  8522  nnawordex  8573  inf0  9542  cantnflt  9593  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  r1ordg  9702  r1val1  9710  rankr1id  9786  acacni  10063  dfacacn  10064  dfac13  10065  ttukeylem5  10435  ttukeylem6  10436  gch2  10598  gch3  10599  gchac  10604  gchina  10622  swrds1  14629  wrdl3s3  14924  sadcp1  16424  lcmfunsnlem2  16609  fnpr2ob  17522  idfucl  17848  gsumval2  18654  gsumz  18804  frmdmnd  18827  frmd0  18828  efginvrel2  19702  efgcpbl2  19732  pgpfaclem1  20058  lbsexg  21162  zringndrg  21448  frlmlbs  21777  mat0dimscm  22434  mat0scmat  22503  m2detleiblem5  22590  m2detleiblem6  22591  m2detleiblem3  22594  m2detleiblem4  22595  d0mat2pmat  22703  chpmat0d  22799  dfac14  23583  acufl  23882  cnextfvval  24030  cnextcn  24032  minveclem3b  25395  minveclem4a  25397  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun2  25473  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  itg2monolem1  25717  itg2mono  25720  itg2cnlem1  25728  xrlimcnp  26932  efrlim  26933  eengbas  29050  ebtwntg  29051  ecgrtg  29052  elntg  29053  wlkl1loop  29706  elwwlks2ons3im  30022  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  2clwwlk2clwwlk  30420  ex-br  30501  trsp2cyc  33184  cyc3evpm  33211  ply1dg1rtn0  33641  lvecdim0  33751  extdg1id  33810  irngss  33831  rge0scvg  34093  repr0  34755  hgt750lemg  34798  r1wf  35239  mrsub0  35698  elmrsubrn  35702  topjoin  36547  finorwe  37698  pclfinN  40346  aomclem1  43482  dfac21  43494  naddgeoa  43822  clsk1indlem1  44472  mnurndlem1  44708  fourierdlem102  46636  fourierdlem114  46648  cycl3grtri  48423  lincval0  48891  lcoel0  48904  discsubc  49539  prsthinc  49939  isinito2lem  49973  termcarweu  50003  diag1f1o  50009  diag2f1o  50012  initocmd  50144