Theorem eqeltri 2266

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 2259	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 146	1 |- A e. C

Syntax hints:   = wceq 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eqeltrri  2267  3eltr4i  2275  intab  3900  inex2  4165  vpwex  4209  ord3ex  4220  uniopel  4286  onsucelsucexmid  4563  nnpredcl  4656  elvvuni  4724  isarep2  5342  acexmidlemcase  5914  abrexex2  6178  oprabex  6182  oprabrexex2  6184  mpoexw  6268  rdg0  6442  frecex  6449  1on  6478  2on  6480  3on  6482  4on  6483  1onn  6575  2onn  6576  3onn  6577  4onn  6578  mapsnf1o2  6752  exmidpw  6966  exmidpw2en  6970  unfiexmid  6976  xpfi  6988  ssfirab  6992  fnfi  6997  iunfidisj  7007  fidcenumlemr  7016  sbthlemi10  7027  ctmlemr  7169  nninfex  7182  exmidonfinlem  7255  acfun  7269  exmidaclem  7270  pw1ne1  7291  ccfunen  7326  nqex  7425  nq0ex  7502  1pr  7616  ltexprlempr  7670  recexprlempr  7694  cauappcvgprlemcl  7715  caucvgprlemcl  7738  caucvgprprlemcl  7766  addvalex  7906  peano1nnnn  7914  peano2nnnn  7915  axcnex  7921  ax1cn  7923  ax1re  7924  pnfxr  8074  mnfxr  8078  inelr  8605  cju  8982  2re  9054  3re  9058  4re  9061  5re  9063  6re  9065  7re  9067  8re  9069  9re  9071  2nn  9146  3nn  9147  4nn  9148  5nn  9149  6nn  9150  7nn  9151  8nn  9152  9nn  9153  nn0ex  9249  nneoor  9422  zeo  9425  deccl  9465  decnncl  9470  numnncl2  9473  decnncl2  9474  numsucc  9490  numma2c  9496  numadd  9497  numaddc  9498  nummul1c  9499  nummul2c  9500  xnegcl  9901  xrex  9925  ioof  10040  uzennn  10510  xnn0nnen  10511  seqex  10523  m1expcl2  10635  faccl  10809  facwordi  10814  faclbnd2  10816  bccl  10841  crre  11004  remim  11007  absval  11148  climle  11480  climcvg1nlem  11495  iserabs  11621  geo2lim  11662  prodfclim1  11690  fprodle  11786  ere  11816  ege2le3  11817  eftlub  11836  efsep  11837  tan0  11877  ef01bndlem  11902  nn0o  12051  pczpre  12438  pockthi  12499  igz  12515  ennnfonelemj0  12561  ennnfonelem0  12565  ndxarg  12644  ndxslid  12646  strndxid  12649  basendxnn  12677  strle1g  12727  plusgndxnn  12732  2strbasg  12740  2stropg  12741  tsetndxnn  12809  plendxnn  12823  dsndxnn  12834  unifndxnn  12844  rmodislmodlem  13849  rmodislmod  13850  cndsex  14052  znval  14135  znle  14136  znbaslemnn  14138  znbas  14143  znzrhval  14146  psrval  14163  fczpsrbag  14168  setsmsbasg  14658  cnbl0  14713  cnopncntop  14723  cnopn  14724  remet  14727  divcnap  14744  expcn  14748  climcncf  14763  idcncf  14780  expcncf  14788  cnrehmeocntop  14789  hovercncf  14825  plyrecj  14941  sincn  14945  coscn  14946  2logb9irrALT  15147  2irrexpq  15149  2irrexpqap  15151  lgslem4  15160  lgsdir2lem2  15186  bdinex2  15462  bj-inex  15469  012of  15556  2o01f  15557  peano3nninf  15567  cvgcmp2nlemabs  15592  trilpolemisumle  15598