Theorem eleqtrri 2528

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 2460	. 2 |- B = C
4	1, 3	eleqtri 2527	1 |- A e. C

Syntax hints:   = wceq 1447   e. wcel 1890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-ext 2431

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1667  df-cleq 2444  df-clel 2447

This theorem is referenced by:  3eltr4i  2542  opi1  4641  opi2  4642  wfrlem14  7035  wfrlem16  7037  seqomlem3  7155  oneo  7268  nnneo  7338  0elixp  7539  ac6sfi  7801  tz9.13  8248  rankval  8273  rankid  8290  ssrankr1  8292  rankel  8296  rankval3  8297  rankpw  8300  rankss  8306  ranksn  8311  rankuni2  8312  rankun  8313  rankpr  8314  rankop  8315  rankeq0  8318  rankr1b  8321  fin1a2lem4  8819  fin1a2lem6  8821  hsmexlem6  8847  dcomex  8863  axdc3lem4  8869  canthp1lem2  9064  pwxpndom2  9076  rankcf  9188  grutsk  9233  axgroth3  9242  inaprc  9247  1lt2pi  9316  1nn  10608  pnfxr  11401  mnfxr  11403  uzrdg0i  12166  axdc4uzlem  12188  ccat2s1p2  12760  infcvgaux1i  13925  0bits  14423  sadcf  14437  prmreclem6  14875  xpsfrnel2  15481  setcepi  15993  grpss  16697  psgnunilem2  17146  psgnprfval2  17174  efgi0  17380  efgi1  17381  vrgpf  17428  vrgpinv  17429  frgpuptinv  17431  frgpup2  17436  frgpnabllem1  17519  dmdprdpr  17692  dprdpr  17693  m2detleiblem3  19664  m2detleiblem4  19665  m2detleib  19666  leordtval2  20238  xpstopnlem1  20834  xpstopnlem2  20836  ptcmp  21083  tsmsfbas  21152  zcld  21841  sszcld  21845  abscncfALT  21962  iimulcn  21976  icopnfhmeo  21981  iccpnfhmeo  21983  xrhmeo  21984  dveflem  22942  ftc1  23005  efopnlem2  23613  cxpcn3  23699  efrlim  23906  usgraex0elv  25134  usgraex1elv  25135  usgraex2elv  25136  usgraex3elv  25137  wlkntrllem1  25300  usgra2adedgwlkonALT  25355  usgra2wlkspthlem2  25359  el2wlkonotlem  25601  usg2wlkonot  25622  usg2wotspth  25623  konigsberg  25726  hhshsslem2  26930  nonbooli  27315  nmopadjlei  27752  fzto1st  28622  xrge0iifhmeo  28748  dya2iocbrsiga  29102  dya2icobrsiga  29103  fib0  29237  fib1  29238  coinflippvt  29322  signstfvn  29463  bnj97  29682  bnj553  29714  bnj966  29760  bnj1442  29863  subfacp1lem2a  29908  subfacp1lem5  29912  erdszelem5  29923  erdszelem8  29926  rankeq1o  30943  0hf  30949  onint1  31114  bj-0eltag  31573  bj-minftyccb  31668  finxpreclem4  31787  fdc  32075  reheibor  32172  pw2f1ocnv  35893  comptiunov2i  36299  corclrcl  36300  sucidALTVD  37263  sucidALT  37264  sucidVD  37265  rfcnpre1  37336  iocopn  37661  icoopn  37666  islptre  37740  icccncfext  37806  fourierdlem103  38129  fourierdlem104  38130  usgra2pthspth  39989  0even  40255  2even  40257  2zrngamgm  40263  zlmodzxzldeplem3  40619