Theorem eqeltri 2187

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

Syntax hints:   = wceq 1314   e. wcel 1463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  eqeltrri  2188  3eltr4i  2196  intab  3766  inex2  4023  vpwex  4063  ord3ex  4074  uniopel  4138  onsucelsucexmid  4405  nnpredcl  4496  elvvuni  4563  isarep2  5168  acexmidlemcase  5723  abrexex2  5976  oprabex  5980  oprabrexex2  5982  rdg0  6238  frecex  6245  1on  6274  2on  6276  3on  6278  4on  6279  1onn  6370  2onn  6371  3onn  6372  4onn  6373  mapsnf1o2  6544  exmidpw  6755  unfiexmid  6759  xpfi  6771  ssfirab  6774  fnfi  6777  iunfidisj  6786  fidcenumlemr  6795  sbthlemi10  6806  ctmlemr  6945  acfun  7011  exmidaclem  7012  ccfunen  7027  nqex  7119  nq0ex  7196  1pr  7310  ltexprlempr  7364  recexprlempr  7388  cauappcvgprlemcl  7409  caucvgprlemcl  7432  caucvgprprlemcl  7460  addvalex  7579  peano1nnnn  7587  peano2nnnn  7588  axcnex  7594  ax1cn  7596  ax1re  7597  pnfxr  7742  mnfxr  7746  inelr  8264  cju  8629  2re  8700  3re  8704  4re  8707  5re  8709  6re  8711  7re  8713  8re  8715  9re  8717  2nn  8785  3nn  8786  4nn  8787  5nn  8788  6nn  8789  7nn  8790  8nn  8791  9nn  8792  nn0ex  8887  nneoor  9057  zeo  9060  deccl  9100  decnncl  9105  numnncl2  9108  decnncl2  9109  numsucc  9125  numma2c  9131  numadd  9132  numaddc  9133  nummul1c  9134  nummul2c  9135  xnegcl  9508  xrex  9532  ioof  9647  uzennn  10102  seqex  10113  m1expcl2  10208  faccl  10374  facwordi  10379  faclbnd2  10381  bccl  10406  crre  10522  remim  10525  absval  10665  climle  10995  climcvg1nlem  11010  iserabs  11136  geo2lim  11177  ere  11227  ege2le3  11228  eftlub  11247  efsep  11248  tan0  11289  ef01bndlem  11314  nn0o  11452  ennnfonelemj0  11759  ennnfonelem0  11763  ndxarg  11825  ndxslid  11827  strndxid  11830  basendxnn  11857  strle1g  11892  2strbasg  11903  2stropg  11904  setsmsbasg  12468  cnbl0  12523  remet  12526  divcnap  12541  climcncf  12557  expcncf  12578  bdinex2  12790  bj-inex  12797  peano3nninf  12893  nninfex  12897  isomninnlem  12917  cvgcmp2nlemabs  12919  trilpolemisumle  12923