Theorem eqeltri 2250

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

Syntax hints:   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrri  2251  3eltr4i  2259  intab  3873  inex2  4137  vpwex  4178  ord3ex  4189  uniopel  4255  onsucelsucexmid  4528  nnpredcl  4621  elvvuni  4689  isarep2  5302  acexmidlemcase  5867  abrexex2  6122  oprabex  6126  oprabrexex2  6128  mpoexw  6211  rdg0  6385  frecex  6392  1on  6421  2on  6423  3on  6425  4on  6426  1onn  6518  2onn  6519  3onn  6520  4onn  6521  mapsnf1o2  6693  exmidpw  6905  unfiexmid  6914  xpfi  6926  ssfirab  6930  fnfi  6933  iunfidisj  6942  fidcenumlemr  6951  sbthlemi10  6962  ctmlemr  7104  nninfex  7117  exmidonfinlem  7189  acfun  7203  exmidaclem  7204  pw1ne1  7225  ccfunen  7260  nqex  7359  nq0ex  7436  1pr  7550  ltexprlempr  7604  recexprlempr  7628  cauappcvgprlemcl  7649  caucvgprlemcl  7672  caucvgprprlemcl  7700  addvalex  7840  peano1nnnn  7848  peano2nnnn  7849  axcnex  7855  ax1cn  7857  ax1re  7858  pnfxr  8006  mnfxr  8010  inelr  8537  cju  8914  2re  8985  3re  8989  4re  8992  5re  8994  6re  8996  7re  8998  8re  9000  9re  9002  2nn  9076  3nn  9077  4nn  9078  5nn  9079  6nn  9080  7nn  9081  8nn  9082  9nn  9083  nn0ex  9178  nneoor  9351  zeo  9354  deccl  9394  decnncl  9399  numnncl2  9402  decnncl2  9403  numsucc  9419  numma2c  9425  numadd  9426  numaddc  9427  nummul1c  9428  nummul2c  9429  xnegcl  9828  xrex  9852  ioof  9967  uzennn  10431  seqex  10442  m1expcl2  10537  faccl  10708  facwordi  10713  faclbnd2  10715  bccl  10740  crre  10859  remim  10862  absval  11003  climle  11335  climcvg1nlem  11350  iserabs  11476  geo2lim  11517  prodfclim1  11545  fprodle  11641  ere  11671  ege2le3  11672  eftlub  11691  efsep  11692  tan0  11732  ef01bndlem  11757  nn0o  11904  pczpre  12289  pockthi  12348  igz  12364  ennnfonelemj0  12394  ennnfonelem0  12398  ndxarg  12477  ndxslid  12479  strndxid  12482  basendxnn  12510  strle1g  12557  plusgndxnn  12562  2strbasg  12570  2stropg  12571  tsetndxnn  12636  plendxnn  12650  dsndxnn  12661  unifndxnn  12671  setsmsbasg  13850  cnbl0  13905  cnopncntop  13908  remet  13911  divcnap  13926  climcncf  13942  expcncf  13963  cnrehmeocntop  13964  sincn  14061  coscn  14062  2logb9irrALT  14263  2irrexpq  14265  2irrexpqap  14267  lgslem4  14275  lgsdir2lem2  14301  bdinex2  14512  bj-inex  14519  012of  14605  2o01f  14606  peano3nninf  14616  cvgcmp2nlemabs  14640  trilpolemisumle  14646