Theorem eleqtrrid 2867

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  rabsnt  4688  onnev  6494  opabiota  6972  canth  7378  onnseq  8359  tfrlem16  8408  oen0  8602  nnawordex  8653  inf0  9629  cantnflt  9680  cnfcom2  9710  cnfcom3lem  9711  cnfcom3  9712  r1ordg  9792  r1val1  9800  r1wf  9848  rankr1id  9885  acacni  10226  dfacacn  10227  dfac13  10228  ttukeylem5  10598  ttukeylem6  10599  gch2  10767  gch3  10768  gchac  10773  gchina  10791  swrds1  14824  wrdl3s3  15124  sadcp1  16634  lcmfunsnlem2  16824  fnpr2ob  17739  idfucl  18065  gsumval2  18884  gsumz  19041  frmdmnd  19064  frmd0  19065  efginvrel2  19950  efgcpbl2  19980  pgpfaclem1  20306  lbsexg  21451  zringndrg  21783  frlmlbs  22112  mat0dimscm  22793  mat0scmat  22862  m2detleiblem5  22949  m2detleiblem6  22950  m2detleiblem3  22953  m2detleiblem4  22954  d0mat2pmat  23065  chpmat0d  23161  dfac14  23946  acufl  24245  cnextfvval  24393  cnextcn  24395  minveclem3b  25758  minveclem4a  25760  ovollb2  25819  ovolunlem1a  25826  ovolunlem1  25827  ovoliunlem1  25832  ovoliun2  25836  ioombl1lem4  25891  uniioombllem1  25911  uniioombllem2  25913  uniioombllem6  25918  itg2monolem1  26080  itg2mono  26083  itg2cnlem1  26091  xrlimcnp  27305  efrlim  27306  eengbas  29568  ebtwntg  29569  ecgrtg  29570  elntg  29571  wlkl1loop  30227  elwwlks2ons3im  30552  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  2clwwlk2clwwlk  30960  ex-br  31041  trsp2cyc  33734  cyc3evpm  33761  dflring3  34079  ply1dg1rtn0  34163  lvecdim0  34289  extdg1id  34348  irngss  34369  rge0scvg  34631  repr0  35290  hgt750lemg  35333  onvfowev  35973  mrsub0  36371  elmrsubrn  36375  topjoin  37249  finorwe  38414  pclfinN  41066  aomclem1  44165  dfac21  44177  naddgeoa  44505  clsk1indlem1  45154  mnurndlem1  45374  fourierdlem102  47326  fourierdlem114  47338  cycl3grtri  49153  lincval0  49635  lcoel0  49648  discsubc  50286  prsthinc  50707  isinito2lem  50741  termcarweu  50771  diag1f1o  50777  diag2f1o  50783  parhomid2  50859  parhomid  50860  initocmd  50960