Theorem eleqtrri 2843

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 2749	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2842	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  3eltr4i  2857  vex  3492  opi1  5488  opi2  5489  frrlem14  8340  wfrlem14OLD  8378  wfrlem16OLD  8380  seqomlem3  8508  nlim2  8546  oneo  8637  nnneo  8711  0elixp  8987  ac6sfi  9348  tz9.13  9860  rankval  9885  rankid  9902  ssrankr1  9904  rankel  9908  rankval3  9909  rankpw  9912  rankss  9918  ranksn  9923  rankuni2  9924  rankun  9925  rankpr  9926  rankop  9927  rankeq0  9930  rankr1b  9933  djuun  9995  dju1dif  10242  isfin4p1  10384  fin1a2lem4  10472  fin1a2lem6  10474  hsmexlem6  10500  dcomex  10516  axdc3lem4  10522  canthp1lem2  10722  pwxpndom2  10734  rankcf  10846  grutsk  10891  axgroth3  10900  inaprc  10905  1lt2pi  10974  pnfxr  11344  mnfxr  11347  1nn  12304  uzrdg0i  14010  axdc4uzlem  14034  ccat2s1p2  14678  wrdl3s3  15011  infcvgaux1i  15905  0bits  16485  sadcf  16499  prmreclem6  16968  fnpr2ob  17618  setcepi  18155  setc2obas  18161  setc2ohom  18162  cat1  18164  smndex1mnd  18945  smndex1id  18946  pwmnd  18972  grpss  18994  psgnunilem2  19537  psgnprfval2  19565  efgi0  19762  efgi1  19763  vrgpf  19810  vrgpinv  19811  frgpuptinv  19813  frgpup2  19818  frgpnabllem1  19915  dmdprdpr  20093  dprdpr  20094  pzriprnglem7  21521  pzriprnglem13  21527  pzriprng1ALT  21530  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  leordtval2  23241  xpstopnlem1  23838  xpstopnlem2  23840  ptcmp  24087  tsmsfbas  24157  zcld  24854  sszcld  24858  abscncfALT  24970  iimulcn  24986  iimulcnOLD  24987  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnstrcvs  25193  cncvs  25197  dveflem  26037  ftc1  26103  efopnlem2  26717  cxpcn3  26809  efrlim  27030  efrlimOLD  27031  precsexlem11  28259  1nns  28370  structvtxval  29056  usgrexmplef  29294  wwlks2onv  29986  elwwlks2ons3im  29987  umgrwwlks2on  29990  konigsberglem4  30287  hhshsslem2  31300  nonbooli  31683  nmopadjlei  32120  cshw1s2  32927  fzto1st  33096  cyc2fv1  33114  cyc3fv1  33130  cyc3fv2  33131  cyc3evpm  33143  1arithidom  33530  zringpid  33545  xrge0iifhmeo  33882  dya2iocbrsiga  34240  dya2icobrsiga  34241  fib0  34364  fib1  34365  coinflippvt  34449  prodfzo03  34580  circlevma  34619  circlemethhgt  34620  hgt750lemg  34631  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgt  34640  bnj97  34842  bnj553  34874  bnj966  34920  bnj1442  35025  subfacp1lem2a  35148  subfacp1lem5  35152  erdszelem5  35163  erdszelem8  35166  ex-sategoelel12  35395  rankeq1o  36135  0hf  36141  onint1  36415  bj-0eltag  36944  bj-minftyccb  37191  finxpreclem4  37360  fdc  37705  reheibor  37799  0prjspnlem  42578  0prjspnrel  42582  pw2f1ocnv  42994  onexoegt  43205  2omomeqom  43265  omnord1ex  43266  oege2  43269  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  comptiunov2i  43668  clsk1indlem4  44006  clsk1indlem1  44007  mnuprdlem3  44243  sucidALTVD  44841  sucidALT  44842  sucidVD  44843  rfcnpre1  44919  eliuniincex  45011  iocopn  45438  icoopn  45443  islptre  45540  cnrefiisplem  45750  icccncfext  45808  fourierdlem103  46130  fourierdlem104  46131  iooborel  46272  upwordnul  46799  upwordsing  46803  sprsymrelfo  47371  sbgoldbo  47661  0even  47960  2even  47962  2zrngamgm  47968  zlmodzxzldeplem3  48231  rrx2pxel  48445  rrx2pyel  48446  rrx2linesl  48477  2sphere0  48484  i0oii  48599  io1ii  48600