Theorem eqeltri 2269

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

Syntax hints:   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eqeltrri  2270  3eltr4i  2278  intab  3903  inex2  4168  vpwex  4212  ord3ex  4223  uniopel  4289  onsucelsucexmid  4566  nnpredcl  4659  elvvuni  4727  isarep2  5345  acexmidlemcase  5917  abrexex2  6181  oprabex  6185  oprabrexex2  6187  mpoexw  6271  rdg0  6445  frecex  6452  1on  6481  2on  6483  3on  6485  4on  6486  1onn  6578  2onn  6579  3onn  6580  4onn  6581  mapsnf1o2  6755  exmidpw  6969  exmidpw2en  6973  unfiexmid  6979  xpfi  6993  ssfirab  6997  fnfi  7002  iunfidisj  7012  fidcenumlemr  7021  sbthlemi10  7032  ctmlemr  7174  nninfex  7187  exmidonfinlem  7260  acfun  7274  exmidaclem  7275  pw1ne1  7296  ccfunen  7331  nqex  7430  nq0ex  7507  1pr  7621  ltexprlempr  7675  recexprlempr  7699  cauappcvgprlemcl  7720  caucvgprlemcl  7743  caucvgprprlemcl  7771  addvalex  7911  peano1nnnn  7919  peano2nnnn  7920  axcnex  7926  ax1cn  7928  ax1re  7929  pnfxr  8079  mnfxr  8083  inelr  8611  cju  8988  2re  9060  3re  9064  4re  9067  5re  9069  6re  9071  7re  9073  8re  9075  9re  9077  2nn  9152  3nn  9153  4nn  9154  5nn  9155  6nn  9156  7nn  9157  8nn  9158  9nn  9159  nn0ex  9255  nneoor  9428  zeo  9431  deccl  9471  decnncl  9476  numnncl2  9479  decnncl2  9480  numsucc  9496  numma2c  9502  numadd  9503  numaddc  9504  nummul1c  9505  nummul2c  9506  xnegcl  9907  xrex  9931  ioof  10046  uzennn  10528  xnn0nnen  10529  seqex  10541  m1expcl2  10653  faccl  10827  facwordi  10832  faclbnd2  10834  bccl  10859  crre  11022  remim  11025  absval  11166  climle  11499  climcvg1nlem  11514  iserabs  11640  geo2lim  11681  prodfclim1  11709  fprodle  11805  ere  11835  ege2le3  11836  eftlub  11855  efsep  11856  tan0  11896  ef01bndlem  11921  nn0o  12072  pczpre  12466  pockthi  12527  igz  12543  ennnfonelemj0  12618  ennnfonelem0  12622  ndxarg  12701  ndxslid  12703  strndxid  12706  basendxnn  12734  strle1g  12784  plusgndxnn  12789  2strbasg  12797  2stropg  12798  tsetndxnn  12866  plendxnn  12880  dsndxnn  12891  unifndxnn  12901  rmodislmodlem  13906  rmodislmod  13907  cndsex  14109  znval  14192  znle  14193  znbaslemnn  14195  znbas  14200  znzrhval  14203  psrval  14220  fczpsrbag  14225  setsmsbasg  14715  cnbl0  14770  cnopncntop  14780  cnopn  14781  remet  14784  divcnap  14801  expcn  14805  climcncf  14820  idcncf  14837  expcncf  14845  cnrehmeocntop  14846  hovercncf  14882  plyrecj  14999  sincn  15005  coscn  15006  2logb9irrALT  15210  2irrexpq  15212  2irrexpqap  15214  lgslem4  15244  lgsdir2lem2  15270  bdinex2  15546  bj-inex  15553  012of  15640  2o01f  15641  peano3nninf  15651  cvgcmp2nlemabs  15676  trilpolemisumle  15682