Theorem eleqtrri 2506

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-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 2437	. 2 |- B = C
4	1, 3	eleqtri 2505	1 |- A e. C

Syntax hints:   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  3eltr4i  2512  opi1  4547  opi2  4548  seqomlem3  6893  oneo  7008  nnneo  7078  0elixp  7282  ac6sfi  7544  tz9.13  7986  rankval  8011  rankid  8028  ssrankr1  8030  rankel  8034  rankval3  8035  rankpw  8038  rankss  8044  ranksn  8049  rankuni2  8050  rankun  8051  rankpr  8052  rankop  8053  rankeq0  8056  rankr1b  8059  fin1a2lem4  8560  fin1a2lem6  8562  hsmexlem6  8588  dcomex  8604  axdc3lem4  8610  canthp1lem2  8808  pwxpndom2  8820  rankcf  8932  grutsk  8977  axgroth3  8986  inaprc  8991  1lt2pi  9062  1nn  10321  pnfxr  11080  mnfxr  11082  uzrdg0i  11766  axdc4uzlem  11788  eqs1  12284  infcvgaux1i  13302  0bits  13618  sadcf  13632  prmreclem6  13965  xpsfrnel2  14486  setcepi  14939  grpss  15539  psgnunilem2  15981  psgnprfval2  16007  efgi0  16197  efgi1  16198  vrgpf  16245  vrgpinv  16246  frgpuptinv  16248  frgpup2  16253  frgpnabllem1  16331  dmdprdpr  16522  dprdpr  16523  m2detleiblem3  18277  m2detleiblem4  18278  m2detleib  18279  leordtval2  18658  xpstopnlem1  19224  xpstopnlem2  19226  ptcmp  19472  tsmsfbas  19540  zcld  20232  sszcld  20236  abscncfALT  20338  iimulcn  20352  icopnfhmeo  20357  iccpnfhmeo  20359  xrhmeo  20360  dveflem  21293  ftc1  21356  efopnlem2  21987  cxpcn3  22071  efrlim  22248  usgraex0elv  23137  usgraex1elv  23138  usgraex2elv  23139  usgraex3elv  23140  wlkntrllem1  23281  konigsberg  23431  hhshsslem2  24492  nonbooli  24877  nmopadjlei  25315  xrge0iifhmeo  26220  dya2iocbrsiga  26544  dya2icobrsiga  26545  fib0  26630  fib1  26631  coinflippvt  26715  signstfvn  26818  subfacp1lem2a  26916  subfacp1lem5  26920  erdszelem5  26931  erdszelem8  26934  wfrlem14  27584  wfrlem16  27586  rankeq1o  28056  0hf  28062  onint1  28143  fdc  28485  reheibor  28582  pw2f1ocnv  29231  rfcnpre1  29586  ccat2s1p2  30112  usgra2pthspth  30141  usgra2wlkspthlem2  30143  el2wlkonotlem  30227  usg2wlkonot  30248  usg2wotspth  30249  zlmodzxzldeplem3  30753  sucidALTVD  31308  sucidALT  31309  sucidVD  31310  bnj97  31561  bnj553  31593  bnj966  31639  bnj1442  31742  bj-0eltag  32054  bj-minftyccb  32128