Theorem eleqtrri 2541

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

Hypotheses

Ref	Expression
eleqtrr.1	|- A e. B
eleqtrr.2	|- C = B

Assertion

Ref	Expression
eleqtrri	|- A e. C

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 |- A e. B
2		eleqtrr.2	. . 3 |- C = B
3	2	eqcomi 2467	. 2 |- B = C
4	1, 3	eleqtri 2540	1 |- A e. C

Syntax hints:   = wceq 1398   e. wcel 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449

This theorem is referenced by:  3eltr4i  2555  opi1  4704  opi2  4705  seqomlem3  7109  oneo  7222  nnneo  7292  0elixp  7493  ac6sfi  7756  tz9.13  8200  rankval  8225  rankid  8242  ssrankr1  8244  rankel  8248  rankval3  8249  rankpw  8252  rankss  8258  ranksn  8263  rankuni2  8264  rankun  8265  rankpr  8266  rankop  8267  rankeq0  8270  rankr1b  8273  fin1a2lem4  8774  fin1a2lem6  8776  hsmexlem6  8802  dcomex  8818  axdc3lem4  8824  canthp1lem2  9020  pwxpndom2  9032  rankcf  9144  grutsk  9189  axgroth3  9198  inaprc  9203  1lt2pi  9272  1nn  10542  pnfxr  11324  mnfxr  11326  uzrdg0i  12052  axdc4uzlem  12074  ccat2s1p2  12622  infcvgaux1i  13750  0bits  14173  sadcf  14187  prmreclem6  14523  xpsfrnel2  15054  setcepi  15566  grpss  16270  psgnunilem2  16719  psgnprfval2  16747  efgi0  16937  efgi1  16938  vrgpf  16985  vrgpinv  16986  frgpuptinv  16988  frgpup2  16993  frgpnabllem1  17076  dmdprdpr  17293  dprdpr  17294  m2detleiblem3  19298  m2detleiblem4  19299  m2detleib  19300  leordtval2  19880  xpstopnlem1  20476  xpstopnlem2  20478  ptcmp  20724  tsmsfbas  20792  zcld  21484  sszcld  21488  abscncfALT  21590  iimulcn  21604  icopnfhmeo  21609  iccpnfhmeo  21611  xrhmeo  21612  dveflem  22546  ftc1  22609  efopnlem2  23206  cxpcn3  23290  efrlim  23497  usgraex0elv  24598  usgraex1elv  24599  usgraex2elv  24600  usgraex3elv  24601  wlkntrllem1  24763  usgra2adedgwlkonALT  24818  usgra2wlkspthlem2  24822  el2wlkonotlem  25064  usg2wlkonot  25085  usg2wotspth  25086  konigsberg  25189  hhshsslem2  26382  nonbooli  26767  nmopadjlei  27205  xrge0iifhmeo  28153  dya2iocbrsiga  28483  dya2icobrsiga  28484  fib0  28602  fib1  28603  coinflippvt  28687  signstfvn  28790  subfacp1lem2a  28888  subfacp1lem5  28892  erdszelem5  28903  erdszelem8  28906  wfrlem14  29596  wfrlem16  29598  rankeq1o  30056  0hf  30062  onint1  30142  fdc  30478  reheibor  30575  pw2f1ocnv  31218  rfcnpre1  31634  iocopn  31799  icoopn  31804  islptre  31864  icccncfext  31929  fourierdlem103  32231  fourierdlem104  32232  usgra2pthspth  32723  0even  32991  2even  32993  2zrngamgm  32999  zlmodzxzldeplem3  33357  sucidALTVD  34071  sucidALT  34072  sucidVD  34073  bnj97  34325  bnj553  34357  bnj966  34403  bnj1442  34506  bj-0eltag  34937  bj-minftyccb  35028  comptiunov2i  38216  corclrcl  38230