Theorem eleqtrri 2858

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtrri.1	⊢ 𝐴 ∈ 𝐵
eleqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrri.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2787	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2857	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1601   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774

This theorem is referenced by:  3eltr4i  2872  opi1  5170  opi2  5171  wfrlem14  7713  wfrlem16  7715  seqomlem3  7832  oneo  7947  nnneo  8017  0elixp  8227  ac6sfi  8494  tz9.13  8953  rankval  8978  rankid  8995  ssrankr1  8997  rankel  9001  rankval3  9002  rankpw  9005  rankss  9011  ranksn  9016  rankuni2  9017  rankun  9018  rankpr  9019  rankop  9020  rankeq0  9023  rankr1b  9026  djuun  9087  fin1a2lem4  9562  fin1a2lem6  9564  hsmexlem6  9590  dcomex  9606  axdc3lem4  9612  canthp1lem2  9812  pwxpndom2  9824  rankcf  9936  grutsk  9981  axgroth3  9990  inaprc  9995  1lt2pi  10064  pnfxr  10432  mnfxr  10436  1nn  11391  uzrdg0i  13081  axdc4uzlem  13105  ccat2s1p2  13724  wrdl3s3  14118  infcvgaux1i  14997  0bits  15571  sadcf  15585  prmreclem6  16033  xpsfrnel2  16615  setcepi  17127  grpss  17831  psgnunilem2  18303  psgnprfval2  18331  efgi0  18521  efgi1  18522  vrgpf  18571  vrgpinv  18572  frgpuptinv  18574  frgpup2  18579  frgpnabllem1  18666  dmdprdpr  18839  dprdpr  18840  m2detleiblem3  20844  m2detleiblem4  20845  m2detleib  20846  leordtval2  21428  xpstopnlem1  22025  xpstopnlem2  22027  ptcmp  22274  tsmsfbas  22343  zcld  23028  sszcld  23032  abscncfALT  23135  iimulcn  23149  icopnfhmeo  23154  iccpnfhmeo  23156  xrhmeo  23157  cnstrcvs  23352  cncvs  23356  dveflem  24183  ftc1  24246  efopnlem2  24844  cxpcn3  24933  efrlim  25152  structvtxval  26373  usgrexmplef  26610  wwlks2onv  27337  elwwlks2ons3im  27338  umgrwwlks2on  27341  konigsberglem4  27665  hhshsslem2  28701  nonbooli  29086  nmopadjlei  29523  fzto1st  30455  xrge0iifhmeo  30584  dya2iocbrsiga  30939  dya2icobrsiga  30940  fib0  31064  fib1  31065  coinflippvt  31149  signstfvn  31250  prodfzo03  31287  circlevma  31326  circlemethhgt  31327  hgt750lemg  31338  hgt750lemb  31340  hgt750lema  31341  hgt750leme  31342  tgoldbachgtde  31344  tgoldbachgt  31347  bnj97  31539  bnj553  31571  bnj966  31617  bnj1442  31720  subfacp1lem2a  31765  subfacp1lem5  31769  erdszelem5  31780  erdszelem8  31783  rankeq1o  32871  0hf  32877  onint1  33035  bj-0eltag  33542  bj-minftyccb  33706  finxpreclem4  33829  cnfin0  33838  fdc  34170  reheibor  34267  pw2f1ocnv  38573  comptiunov2i  38965  corclrcl  38966  clsk1indlem4  39308  clsk1indlem1  39309  sucidALTVD  40049  sucidALT  40050  sucidVD  40051  rfcnpre1  40121  eliuniincex  40231  iocopn  40665  icoopn  40670  islptre  40769  cnrefiisplem  40979  icccncfext  41038  fourierdlem103  41363  fourierdlem104  41364  iooborel  41503  sprsymrelfo  42446  sbgoldbo  42710  0even  42956  2even  42958  2zrngamgm  42964  zlmodzxzldeplem3  43316  rrx2pxel  43457  rrx2pyel  43458  rrx2linesl  43489  2sphere0  43496