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 1397   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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  3957  inex2  4224  vpwex  4269  ord3ex  4280  uniopel  4349  onsucelsucexmid  4628  nnpredcl  4721  elvvuni  4790  isarep2  5417  acexmidlemcase  6013  abrexex2  6286  oprabex  6290  oprabrexex2  6292  mpoexw  6378  rdg0  6553  frecex  6560  1on  6589  2on  6591  3on  6593  4on  6595  2oex  6599  1onn  6688  2onn  6689  3onn  6690  4onn  6691  mapsnf1o2  6865  exmidpw  7100  exmidpw2en  7104  unfiexmid  7110  xpfi  7124  ssfirab  7129  fnfi  7135  iunfidisj  7145  fidcenumlemr  7154  sbthlemi10  7165  ctmlemr  7307  nninfex  7320  exmidonfinlem  7404  acfun  7422  exmidaclem  7423  pw1ne1  7447  ccfunen  7483  nqex  7583  nq0ex  7660  1pr  7774  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  caucvgprlemcl  7896  caucvgprprlemcl  7924  addvalex  8064  peano1nnnn  8072  peano2nnnn  8073  axcnex  8079  ax1cn  8081  ax1re  8082  pnfxr  8232  mnfxr  8236  inelr  8764  cju  9141  2re  9213  3re  9217  4re  9220  5re  9222  6re  9224  7re  9226  8re  9228  9re  9230  2nn  9305  3nn  9306  4nn  9307  5nn  9308  6nn  9309  7nn  9310  8nn  9311  9nn  9312  nn0ex  9408  nneoor  9582  zeo  9585  deccl  9625  decnncl  9630  numnncl2  9633  decnncl2  9634  numsucc  9650  numma2c  9656  numadd  9657  numaddc  9658  nummul1c  9659  nummul2c  9660  xnegcl  10067  xrex  10091  ioof  10206  uzennn  10699  xnn0nnen  10700  seqex  10712  m1expcl2  10824  faccl  10998  facwordi  11003  faclbnd2  11005  bccl  11030  lswex  11169  crre  11435  remim  11438  absval  11579  climle  11912  climcvg1nlem  11927  iserabs  12054  geo2lim  12095  prodfclim1  12123  fprodle  12219  ere  12249  ege2le3  12250  eftlub  12269  efsep  12270  tan0  12310  ef01bndlem  12335  nn0o  12486  pczpre  12888  pockthi  12949  igz  12965  ennnfonelemj0  13040  ennnfonelem0  13044  ndxarg  13123  ndxslid  13125  strndxid  13128  basendxnn  13156  strle1g  13207  plusgndxnn  13212  2strbasg  13221  2stropg  13222  tsetndxnn  13290  plendxnn  13304  dsndxnn  13319  unifndxnn  13329  rmodislmodlem  14383  rmodislmod  14384  cndsex  14586  znval  14669  znle  14670  znbaslemnn  14672  znbas  14677  znzrhval  14680  psrval  14699  fczpsrbag  14704  setsmsbasg  15222  cnbl0  15277  cnopncntop  15287  cnopn  15288  remet  15291  divcnap  15308  expcn  15312  climcncf  15327  idcncf  15344  expcncf  15352  cnrehmeocntop  15353  hovercncf  15389  plyrecj  15506  sincn  15512  coscn  15513  2logb9irrALT  15717  2irrexpq  15719  2irrexpqap  15721  lgslem4  15751  lgsdir2lem2  15777  edgfndxnn  15878  setsvtx  15921  usgrstrrepeen  16101  eulerpathprum  16350  konigsbergumgr  16357  konigsberglem5  16362  konigsberg  16363  bdinex2  16546  bj-inex  16553  012of  16643  2o01f  16644  peano3nninf  16660  cvgcmp2nlemabs  16687  trilpolemisumle  16693