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  3874  inex2  4139  vpwex  4180  ord3ex  4191  uniopel  4257  onsucelsucexmid  4530  nnpredcl  4623  elvvuni  4691  isarep2  5304  acexmidlemcase  5870  abrexex2  6125  oprabex  6129  oprabrexex2  6131  mpoexw  6214  rdg0  6388  frecex  6395  1on  6424  2on  6426  3on  6428  4on  6429  1onn  6521  2onn  6522  3onn  6523  4onn  6524  mapsnf1o2  6696  exmidpw  6908  unfiexmid  6917  xpfi  6929  ssfirab  6933  fnfi  6936  iunfidisj  6945  fidcenumlemr  6954  sbthlemi10  6965  ctmlemr  7107  nninfex  7120  exmidonfinlem  7192  acfun  7206  exmidaclem  7207  pw1ne1  7228  ccfunen  7263  nqex  7362  nq0ex  7439  1pr  7553  ltexprlempr  7607  recexprlempr  7631  cauappcvgprlemcl  7652  caucvgprlemcl  7675  caucvgprprlemcl  7703  addvalex  7843  peano1nnnn  7851  peano2nnnn  7852  axcnex  7858  ax1cn  7860  ax1re  7861  pnfxr  8010  mnfxr  8014  inelr  8541  cju  8918  2re  8989  3re  8993  4re  8996  5re  8998  6re  9000  7re  9002  8re  9004  9re  9006  2nn  9080  3nn  9081  4nn  9082  5nn  9083  6nn  9084  7nn  9085  8nn  9086  9nn  9087  nn0ex  9182  nneoor  9355  zeo  9358  deccl  9398  decnncl  9403  numnncl2  9406  decnncl2  9407  numsucc  9423  numma2c  9429  numadd  9430  numaddc  9431  nummul1c  9432  nummul2c  9433  xnegcl  9832  xrex  9856  ioof  9971  uzennn  10436  seqex  10447  m1expcl2  10542  faccl  10715  facwordi  10720  faclbnd2  10722  bccl  10747  crre  10866  remim  10869  absval  11010  climle  11342  climcvg1nlem  11357  iserabs  11483  geo2lim  11524  prodfclim1  11552  fprodle  11648  ere  11678  ege2le3  11679  eftlub  11698  efsep  11699  tan0  11739  ef01bndlem  11764  nn0o  11912  pczpre  12297  pockthi  12356  igz  12372  ennnfonelemj0  12402  ennnfonelem0  12406  ndxarg  12485  ndxslid  12487  strndxid  12490  basendxnn  12518  strle1g  12565  plusgndxnn  12570  2strbasg  12578  2stropg  12579  tsetndxnn  12644  plendxnn  12658  dsndxnn  12669  unifndxnn  12679  rmodislmodlem  13440  rmodislmod  13441  setsmsbasg  13982  cnbl0  14037  cnopncntop  14040  remet  14043  divcnap  14058  climcncf  14074  expcncf  14095  cnrehmeocntop  14096  sincn  14193  coscn  14194  2logb9irrALT  14395  2irrexpq  14397  2irrexpqap  14399  lgslem4  14407  lgsdir2lem2  14433  bdinex2  14655  bj-inex  14662  012of  14748  2o01f  14749  peano3nninf  14759  cvgcmp2nlemabs  14783  trilpolemisumle  14789