Theorem eqeltri 2302

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

Syntax hints:   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrri  2303  3eltr4i  2311  intab  3952  inex2  4219  vpwex  4263  ord3ex  4274  uniopel  4343  onsucelsucexmid  4622  nnpredcl  4715  elvvuni  4783  isarep2  5408  acexmidlemcase  5996  abrexex2  6269  oprabex  6273  oprabrexex2  6275  mpoexw  6359  rdg0  6533  frecex  6540  1on  6569  2on  6571  3on  6573  4on  6574  1onn  6666  2onn  6667  3onn  6668  4onn  6669  mapsnf1o2  6843  exmidpw  7070  exmidpw2en  7074  unfiexmid  7080  xpfi  7094  ssfirab  7098  fnfi  7103  iunfidisj  7113  fidcenumlemr  7122  sbthlemi10  7133  ctmlemr  7275  nninfex  7288  exmidonfinlem  7371  acfun  7389  exmidaclem  7390  pw1ne1  7414  ccfunen  7450  nqex  7550  nq0ex  7627  1pr  7741  ltexprlempr  7795  recexprlempr  7819  cauappcvgprlemcl  7840  caucvgprlemcl  7863  caucvgprprlemcl  7891  addvalex  8031  peano1nnnn  8039  peano2nnnn  8040  axcnex  8046  ax1cn  8048  ax1re  8049  pnfxr  8199  mnfxr  8203  inelr  8731  cju  9108  2re  9180  3re  9184  4re  9187  5re  9189  6re  9191  7re  9193  8re  9195  9re  9197  2nn  9272  3nn  9273  4nn  9274  5nn  9275  6nn  9276  7nn  9277  8nn  9278  9nn  9279  nn0ex  9375  nneoor  9549  zeo  9552  deccl  9592  decnncl  9597  numnncl2  9600  decnncl2  9601  numsucc  9617  numma2c  9623  numadd  9624  numaddc  9625  nummul1c  9626  nummul2c  9627  xnegcl  10028  xrex  10052  ioof  10167  uzennn  10658  xnn0nnen  10659  seqex  10671  m1expcl2  10783  faccl  10957  facwordi  10962  faclbnd2  10964  bccl  10989  lswex  11123  crre  11368  remim  11371  absval  11512  climle  11845  climcvg1nlem  11860  iserabs  11986  geo2lim  12027  prodfclim1  12055  fprodle  12151  ere  12181  ege2le3  12182  eftlub  12201  efsep  12202  tan0  12242  ef01bndlem  12267  nn0o  12418  pczpre  12820  pockthi  12881  igz  12897  ennnfonelemj0  12972  ennnfonelem0  12976  ndxarg  13055  ndxslid  13057  strndxid  13060  basendxnn  13088  strle1g  13139  plusgndxnn  13144  2strbasg  13153  2stropg  13154  tsetndxnn  13222  plendxnn  13236  dsndxnn  13251  unifndxnn  13261  rmodislmodlem  14314  rmodislmod  14315  cndsex  14517  znval  14600  znle  14601  znbaslemnn  14603  znbas  14608  znzrhval  14611  psrval  14630  fczpsrbag  14635  setsmsbasg  15153  cnbl0  15208  cnopncntop  15218  cnopn  15219  remet  15222  divcnap  15239  expcn  15243  climcncf  15258  idcncf  15275  expcncf  15283  cnrehmeocntop  15284  hovercncf  15320  plyrecj  15437  sincn  15443  coscn  15444  2logb9irrALT  15648  2irrexpq  15650  2irrexpqap  15652  lgslem4  15682  lgsdir2lem2  15708  edgfndxnn  15809  setsvtx  15852  usgrstrrepeen  16029  bdinex2  16263  bj-inex  16270  012of  16357  2o01f  16358  peano3nninf  16373  cvgcmp2nlemabs  16400  trilpolemisumle  16406