Theorem eleqtrri 2687

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

Hypotheses

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

Assertion

Ref	Expression
eleqtrri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2619	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2686	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  3eltr4i  2701  opi1  4864  opi2  4865  wfrlem14  7315  wfrlem16  7317  seqomlem3  7434  oneo  7548  nnneo  7618  0elixp  7825  ac6sfi  8089  tz9.13  8537  rankval  8562  rankid  8579  ssrankr1  8581  rankel  8585  rankval3  8586  rankpw  8589  rankss  8595  ranksn  8600  rankuni2  8601  rankun  8602  rankpr  8603  rankop  8604  rankeq0  8607  rankr1b  8610  fin1a2lem4  9108  fin1a2lem6  9110  hsmexlem6  9136  dcomex  9152  axdc3lem4  9158  canthp1lem2  9354  pwxpndom2  9366  rankcf  9478  grutsk  9523  axgroth3  9532  inaprc  9537  1lt2pi  9606  pnfxr  9971  mnfxr  9975  1nn  10908  uzrdg0i  12620  axdc4uzlem  12644  ccat2s1p2  13258  wrdl3s3  13553  infcvgaux1i  14428  0bits  14999  sadcf  15013  prmreclem6  15463  xpsfrnel2  16048  setcepi  16561  grpss  17263  psgnunilem2  17738  psgnprfval2  17766  efgi0  17956  efgi1  17957  vrgpf  18004  vrgpinv  18005  frgpuptinv  18007  frgpup2  18012  frgpnabllem1  18099  dmdprdpr  18271  dprdpr  18272  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  leordtval2  20826  xpstopnlem1  21422  xpstopnlem2  21424  ptcmp  21672  tsmsfbas  21741  zcld  22424  sszcld  22428  abscncfALT  22531  iimulcn  22545  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  cnstrcvs  22749  cncvs  22753  dveflem  23546  ftc1  23609  efopnlem2  24203  cxpcn3  24289  efrlim  24496  usgraex0elv  25924  usgraex1elv  25925  usgraex2elv  25926  usgraex3elv  25927  wlkntrllem1  26089  usgra2adedgwlkonALT  26144  usgra2wlkspthlem2  26148  el2wlkonotlem  26389  usg2wlkonot  26410  usg2wotspth  26411  konigsberg  26514  hhshsslem2  27509  nonbooli  27894  nmopadjlei  28331  fzto1st  29184  xrge0iifhmeo  29310  dya2iocbrsiga  29664  dya2icobrsiga  29665  fib0  29788  fib1  29789  coinflippvt  29873  signstfvn  29972  bnj97  30190  bnj553  30222  bnj966  30268  bnj1442  30371  subfacp1lem2a  30416  subfacp1lem5  30420  erdszelem5  30431  erdszelem8  30434  rankeq1o  31448  0hf  31454  onint1  31618  bj-0eltag  32159  bj-minftyccb  32289  finxpreclem4  32407  fdc  32711  reheibor  32808  pw2f1ocnv  36622  comptiunov2i  37017  corclrcl  37018  clsk1indlem4  37362  clsk1indlem1  37363  sucidALTVD  38128  sucidALT  38129  sucidVD  38130  rfcnpre1  38201  eliuniincex  38323  iocopn  38593  icoopn  38598  islptre  38686  icccncfext  38773  fourierdlem103  39102  fourierdlem104  39103  iooborel  39245  umgrwwlks2on  41161  konigsberglem4  41425  0even  41721  2even  41723  2zrngamgm  41729  zlmodzxzldeplem3  42085