Theorem eqeltri 2278

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

Hypotheses

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

Assertion

Ref	Expression
eqeltri	|- A e. C

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 2271	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 146	1 |- A e. C

Syntax hints:   = wceq 1373   e. wcel 2176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrri  2279  3eltr4i  2287  intab  3914  inex2  4179  vpwex  4223  ord3ex  4234  uniopel  4301  onsucelsucexmid  4578  nnpredcl  4671  elvvuni  4739  isarep2  5361  acexmidlemcase  5939  abrexex2  6209  oprabex  6213  oprabrexex2  6215  mpoexw  6299  rdg0  6473  frecex  6480  1on  6509  2on  6511  3on  6513  4on  6514  1onn  6606  2onn  6607  3onn  6608  4onn  6609  mapsnf1o2  6783  exmidpw  7005  exmidpw2en  7009  unfiexmid  7015  xpfi  7029  ssfirab  7033  fnfi  7038  iunfidisj  7048  fidcenumlemr  7057  sbthlemi10  7068  ctmlemr  7210  nninfex  7223  exmidonfinlem  7301  acfun  7319  exmidaclem  7320  pw1ne1  7341  ccfunen  7376  nqex  7476  nq0ex  7553  1pr  7667  ltexprlempr  7721  recexprlempr  7745  cauappcvgprlemcl  7766  caucvgprlemcl  7789  caucvgprprlemcl  7817  addvalex  7957  peano1nnnn  7965  peano2nnnn  7966  axcnex  7972  ax1cn  7974  ax1re  7975  pnfxr  8125  mnfxr  8129  inelr  8657  cju  9034  2re  9106  3re  9110  4re  9113  5re  9115  6re  9117  7re  9119  8re  9121  9re  9123  2nn  9198  3nn  9199  4nn  9200  5nn  9201  6nn  9202  7nn  9203  8nn  9204  9nn  9205  nn0ex  9301  nneoor  9475  zeo  9478  deccl  9518  decnncl  9523  numnncl2  9526  decnncl2  9527  numsucc  9543  numma2c  9549  numadd  9550  numaddc  9551  nummul1c  9552  nummul2c  9553  xnegcl  9954  xrex  9978  ioof  10093  uzennn  10581  xnn0nnen  10582  seqex  10594  m1expcl2  10706  faccl  10880  facwordi  10885  faclbnd2  10887  bccl  10912  crre  11168  remim  11171  absval  11312  climle  11645  climcvg1nlem  11660  iserabs  11786  geo2lim  11827  prodfclim1  11855  fprodle  11951  ere  11981  ege2le3  11982  eftlub  12001  efsep  12002  tan0  12042  ef01bndlem  12067  nn0o  12218  pczpre  12620  pockthi  12681  igz  12697  ennnfonelemj0  12772  ennnfonelem0  12776  ndxarg  12855  ndxslid  12857  strndxid  12860  basendxnn  12888  strle1g  12938  plusgndxnn  12943  2strbasg  12952  2stropg  12953  tsetndxnn  13021  plendxnn  13035  dsndxnn  13050  unifndxnn  13060  rmodislmodlem  14112  rmodislmod  14113  cndsex  14315  znval  14398  znle  14399  znbaslemnn  14401  znbas  14406  znzrhval  14409  psrval  14428  fczpsrbag  14433  setsmsbasg  14951  cnbl0  15006  cnopncntop  15016  cnopn  15017  remet  15020  divcnap  15037  expcn  15041  climcncf  15056  idcncf  15073  expcncf  15081  cnrehmeocntop  15082  hovercncf  15118  plyrecj  15235  sincn  15241  coscn  15242  2logb9irrALT  15446  2irrexpq  15448  2irrexpqap  15450  lgslem4  15480  lgsdir2lem2  15506  edgfndxnn  15607  bdinex2  15836  bj-inex  15843  012of  15930  2o01f  15931  peano3nninf  15944  cvgcmp2nlemabs  15971  trilpolemisumle  15977