Theorem eleqtrri 2547

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

Syntax hints:   = wceq 1374   e. wcel 1762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2452  df-clel 2455

This theorem is referenced by:  3eltr4i  2561  opi1  4707  opi2  4708  seqomlem3  7107  oneo  7220  nnneo  7290  0elixp  7490  ac6sfi  7753  tz9.13  8198  rankval  8223  rankid  8240  ssrankr1  8242  rankel  8246  rankval3  8247  rankpw  8250  rankss  8256  ranksn  8261  rankuni2  8262  rankun  8263  rankpr  8264  rankop  8265  rankeq0  8268  rankr1b  8271  fin1a2lem4  8772  fin1a2lem6  8774  hsmexlem6  8800  dcomex  8816  axdc3lem4  8822  canthp1lem2  9020  pwxpndom2  9032  rankcf  9144  grutsk  9189  axgroth3  9198  inaprc  9203  1lt2pi  9272  1nn  10536  pnfxr  11310  mnfxr  11312  uzrdg0i  12026  axdc4uzlem  12048  eqs1  12571  ccat2s1p2  12583  infcvgaux1i  13620  0bits  13937  sadcf  13951  prmreclem6  14287  xpsfrnel2  14809  setcepi  15262  grpss  15865  psgnunilem2  16309  psgnprfval2  16337  efgi0  16527  efgi1  16528  vrgpf  16575  vrgpinv  16576  frgpuptinv  16578  frgpup2  16583  frgpnabllem1  16661  dmdprdpr  16881  dprdpr  16882  m2detleiblem3  18891  m2detleiblem4  18892  m2detleib  18893  leordtval2  19472  xpstopnlem1  20038  xpstopnlem2  20040  ptcmp  20286  tsmsfbas  20354  zcld  21046  sszcld  21050  abscncfALT  21152  iimulcn  21166  icopnfhmeo  21171  iccpnfhmeo  21173  xrhmeo  21174  dveflem  22108  ftc1  22171  efopnlem2  22759  cxpcn3  22843  efrlim  23020  usgraex0elv  24058  usgraex1elv  24059  usgraex2elv  24060  usgraex3elv  24061  wlkntrllem1  24223  usgra2adedgwlkonALT  24278  usgra2wlkspthlem2  24282  el2wlkonotlem  24524  usg2wlkonot  24545  usg2wotspth  24546  konigsberg  24649  hhshsslem2  25846  nonbooli  26231  nmopadjlei  26669  xrge0iifhmeo  27540  dya2iocbrsiga  27872  dya2icobrsiga  27873  fib0  27964  fib1  27965  coinflippvt  28049  signstfvn  28152  subfacp1lem2a  28250  subfacp1lem5  28254  erdszelem5  28265  erdszelem8  28268  wfrlem14  28919  wfrlem16  28921  rankeq1o  29391  0hf  29397  onint1  29477  fdc  29828  reheibor  29925  pw2f1ocnv  30572  rfcnpre1  30927  iocopn  31079  icoopn  31084  islptre  31116  icccncfext  31181  fourierdlem103  31465  fourierdlem104  31466  usgra2pthspth  31775  zlmodzxzldeplem3  32059  sucidALTVD  32625  sucidALT  32626  sucidVD  32627  bnj97  32878  bnj553  32910  bnj966  32956  bnj1442  33059  bj-0eltag  33492  bj-minftyccb  33575