Theorem eqeltri 2280

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

Syntax hints:   = wceq 1373   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eqeltrri  2281  3eltr4i  2289  intab  3928  inex2  4195  vpwex  4239  ord3ex  4250  uniopel  4319  onsucelsucexmid  4596  nnpredcl  4689  elvvuni  4757  isarep2  5380  acexmidlemcase  5962  abrexex2  6232  oprabex  6236  oprabrexex2  6238  mpoexw  6322  rdg0  6496  frecex  6503  1on  6532  2on  6534  3on  6536  4on  6537  1onn  6629  2onn  6630  3onn  6631  4onn  6632  mapsnf1o2  6806  exmidpw  7031  exmidpw2en  7035  unfiexmid  7041  xpfi  7055  ssfirab  7059  fnfi  7064  iunfidisj  7074  fidcenumlemr  7083  sbthlemi10  7094  ctmlemr  7236  nninfex  7249  exmidonfinlem  7332  acfun  7350  exmidaclem  7351  pw1ne1  7375  ccfunen  7411  nqex  7511  nq0ex  7588  1pr  7702  ltexprlempr  7756  recexprlempr  7780  cauappcvgprlemcl  7801  caucvgprlemcl  7824  caucvgprprlemcl  7852  addvalex  7992  peano1nnnn  8000  peano2nnnn  8001  axcnex  8007  ax1cn  8009  ax1re  8010  pnfxr  8160  mnfxr  8164  inelr  8692  cju  9069  2re  9141  3re  9145  4re  9148  5re  9150  6re  9152  7re  9154  8re  9156  9re  9158  2nn  9233  3nn  9234  4nn  9235  5nn  9236  6nn  9237  7nn  9238  8nn  9239  9nn  9240  nn0ex  9336  nneoor  9510  zeo  9513  deccl  9553  decnncl  9558  numnncl2  9561  decnncl2  9562  numsucc  9578  numma2c  9584  numadd  9585  numaddc  9586  nummul1c  9587  nummul2c  9588  xnegcl  9989  xrex  10013  ioof  10128  uzennn  10618  xnn0nnen  10619  seqex  10631  m1expcl2  10743  faccl  10917  facwordi  10922  faclbnd2  10924  bccl  10949  lswex  11082  crre  11283  remim  11286  absval  11427  climle  11760  climcvg1nlem  11775  iserabs  11901  geo2lim  11942  prodfclim1  11970  fprodle  12066  ere  12096  ege2le3  12097  eftlub  12116  efsep  12117  tan0  12157  ef01bndlem  12182  nn0o  12333  pczpre  12735  pockthi  12796  igz  12812  ennnfonelemj0  12887  ennnfonelem0  12891  ndxarg  12970  ndxslid  12972  strndxid  12975  basendxnn  13003  strle1g  13053  plusgndxnn  13058  2strbasg  13067  2stropg  13068  tsetndxnn  13136  plendxnn  13150  dsndxnn  13165  unifndxnn  13175  rmodislmodlem  14227  rmodislmod  14228  cndsex  14430  znval  14513  znle  14514  znbaslemnn  14516  znbas  14521  znzrhval  14524  psrval  14543  fczpsrbag  14548  setsmsbasg  15066  cnbl0  15121  cnopncntop  15131  cnopn  15132  remet  15135  divcnap  15152  expcn  15156  climcncf  15171  idcncf  15188  expcncf  15196  cnrehmeocntop  15197  hovercncf  15233  plyrecj  15350  sincn  15356  coscn  15357  2logb9irrALT  15561  2irrexpq  15563  2irrexpqap  15565  lgslem4  15595  lgsdir2lem2  15621  edgfndxnn  15722  bdinex2  16035  bj-inex  16042  012of  16130  2o01f  16131  peano3nninf  16146  cvgcmp2nlemabs  16173  trilpolemisumle  16179