Theorem eleqtrri 2914

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

Syntax hints:   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  3eltr4i  2928  vex  3499  opi1  5362  opi2  5363  wfrlem14  7970  wfrlem16  7972  seqomlem3  8090  oneo  8209  nnneo  8280  0elixp  8495  ac6sfi  8764  tz9.13  9222  rankval  9247  rankid  9264  ssrankr1  9266  rankel  9270  rankval3  9271  rankpw  9274  rankss  9280  ranksn  9285  rankuni2  9286  rankun  9287  rankpr  9288  rankop  9289  rankeq0  9292  rankr1b  9295  djuun  9357  dju1dif  9600  isfin4p1  9739  fin1a2lem4  9827  fin1a2lem6  9829  hsmexlem6  9855  dcomex  9871  axdc3lem4  9877  canthp1lem2  10077  pwxpndom2  10089  rankcf  10201  grutsk  10246  axgroth3  10255  inaprc  10260  1lt2pi  10329  pnfxr  10697  mnfxr  10700  1nn  11651  uzrdg0i  13330  axdc4uzlem  13354  ccat2s1p2  13988  ccat2s1p2OLD  13990  wrdl3s3  14328  infcvgaux1i  15214  0bits  15790  sadcf  15804  prmreclem6  16259  fnpr2ob  16833  setcepi  17350  smndex1mnd  18077  smndex1id  18078  pwmnd  18104  grpss  18123  psgnunilem2  18625  psgnprfval2  18653  efgi0  18848  efgi1  18849  vrgpf  18896  vrgpinv  18897  frgpuptinv  18899  frgpup2  18904  frgpnabllem1  18995  dmdprdpr  19173  dprdpr  19174  m2detleiblem3  21240  m2detleiblem4  21241  m2detleib  21242  leordtval2  21822  xpstopnlem1  22419  xpstopnlem2  22421  ptcmp  22668  tsmsfbas  22738  zcld  23423  sszcld  23427  abscncfALT  23530  iimulcn  23544  icopnfhmeo  23549  iccpnfhmeo  23551  xrhmeo  23552  cnstrcvs  23747  cncvs  23751  dveflem  24578  ftc1  24641  efopnlem2  25242  cxpcn3  25331  efrlim  25549  structvtxval  26808  usgrexmplef  27043  wwlks2onv  27734  elwwlks2ons3im  27735  umgrwwlks2on  27738  konigsberglem4  28036  hhshsslem2  29047  nonbooli  29430  nmopadjlei  29867  cshw1s2  30636  fzto1st  30747  cyc2fv1  30765  cyc3fv1  30781  cyc3fv2  30782  cyc3evpm  30794  xrge0iifhmeo  31181  dya2iocbrsiga  31535  dya2icobrsiga  31536  fib0  31659  fib1  31660  coinflippvt  31744  prodfzo03  31876  circlevma  31915  circlemethhgt  31916  hgt750lemg  31927  hgt750lemb  31929  hgt750lema  31930  hgt750leme  31931  tgoldbachgtde  31933  tgoldbachgt  31936  bnj97  32140  bnj553  32172  bnj966  32218  bnj1442  32323  subfacp1lem2a  32429  subfacp1lem5  32433  erdszelem5  32444  erdszelem8  32447  ex-sategoelel12  32676  frrlem14  33138  rankeq1o  33634  0hf  33640  onint1  33799  bj-0eltag  34292  bj-minftyccb  34509  finxpreclem4  34677  fdc  35022  reheibor  35119  0prjspnlem  39275  0prjspnrel  39276  pw2f1ocnv  39641  comptiunov2i  40058  clsk1indlem4  40401  clsk1indlem1  40402  mnuprdlem3  40617  sucidALTVD  41211  sucidALT  41212  sucidVD  41213  rfcnpre1  41283  eliuniincex  41382  iocopn  41803  icoopn  41808  islptre  41907  cnrefiisplem  42117  icccncfext  42177  fourierdlem103  42501  fourierdlem104  42502  iooborel  42641  sprsymrelfo  43666  sbgoldbo  43959  0even  44209  2even  44211  2zrngamgm  44217  zlmodzxzldeplem3  44564  rrx2pxel  44705  rrx2pyel  44706  rrx2linesl  44737  2sphere0  44744