Theorem eqeltri 2304

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

Syntax hints:   = wceq 1398   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrri  2305  3eltr4i  2313  intab  3962  inex2  4229  vpwex  4275  ord3ex  4286  uniopel  4355  onsucelsucexmid  4634  nnpredcl  4727  elvvuni  4796  isarep2  5424  acexmidlemcase  6023  abrexex2  6295  oprabex  6299  oprabrexex2  6301  mpoexw  6387  rdg0  6596  frecex  6603  1on  6632  2on  6634  3on  6636  4on  6638  2oex  6642  1onn  6731  2onn  6732  3onn  6733  4onn  6734  mapsnf1o2  6908  exmidpw  7143  exmidpw2en  7147  unfiexmid  7153  xpfi  7167  ssfirab  7172  fnfi  7178  iunfidisj  7188  fidcenumlemr  7197  sbthlemi10  7208  fczfsuppd  7222  ctmlemr  7367  nninfex  7380  exmidonfinlem  7464  acfun  7482  exmidaclem  7483  pw1ne1  7507  ccfunen  7543  nqex  7643  nq0ex  7720  1pr  7834  ltexprlempr  7888  recexprlempr  7912  cauappcvgprlemcl  7933  caucvgprlemcl  7956  caucvgprprlemcl  7984  addvalex  8124  peano1nnnn  8132  peano2nnnn  8133  axcnex  8139  ax1cn  8141  ax1re  8142  pnfxr  8291  mnfxr  8295  inelr  8823  cju  9200  2re  9272  3re  9276  4re  9279  5re  9281  6re  9283  7re  9285  8re  9287  9re  9289  2nn  9364  3nn  9365  4nn  9366  5nn  9367  6nn  9368  7nn  9369  8nn  9370  9nn  9371  nn0ex  9467  nneoor  9643  zeo  9646  deccl  9686  decnncl  9691  numnncl2  9694  decnncl2  9695  numsucc  9711  numma2c  9717  numadd  9718  numaddc  9719  nummul1c  9720  nummul2c  9721  xnegcl  10128  xrex  10152  ioof  10267  uzennn  10761  xnn0nnen  10762  seqex  10774  m1expcl2  10886  faccl  11060  facwordi  11065  faclbnd2  11067  bccl  11092  lswex  11231  crre  11497  remim  11500  absval  11641  climle  11974  climcvg1nlem  11989  iserabs  12116  geo2lim  12157  prodfclim1  12185  fprodle  12281  ere  12311  ege2le3  12312  eftlub  12331  efsep  12332  tan0  12372  ef01bndlem  12397  nn0o  12548  pczpre  12950  pockthi  13011  igz  13027  ennnfonelemj0  13102  ennnfonelem0  13106  ndxarg  13185  ndxslid  13187  strndxid  13190  basendxnn  13218  strle1g  13269  plusgndxnn  13274  2strbasg  13283  2stropg  13284  tsetndxnn  13352  plendxnn  13366  dsndxnn  13381  unifndxnn  13391  rmodislmodlem  14446  rmodislmod  14447  cndsex  14649  znval  14732  znle  14733  znbaslemnn  14735  znbas  14740  znzrhval  14743  psrval  14762  fczpsrbag  14767  setsmsbasg  15290  cnbl0  15345  cnopncntop  15355  cnopn  15356  remet  15359  divcnap  15376  expcn  15380  climcncf  15395  idcncf  15412  expcncf  15420  cnrehmeocntop  15421  hovercncf  15457  plyrecj  15574  sincn  15580  coscn  15581  2logb9irrALT  15785  2irrexpq  15787  2irrexpqap  15789  lgslem4  15822  lgsdir2lem2  15848  edgfndxnn  15949  setsvtx  15992  usgrstrrepeen  16172  eulerpathprum  16421  konigsbergumgr  16428  konigsberglem5  16433  konigsberg  16434  bdinex2  16616  bj-inex  16623  012of  16713  2o01f  16714  peano3nninf  16733  cvgcmp2nlemabs  16764  trilpolemisumle  16770