Theorem eqeltri 2278

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

Syntax hints:   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrri  2279  3eltr4i  2287  intab  3914  inex2  4180  vpwex  4224  ord3ex  4235  uniopel  4302  onsucelsucexmid  4579  nnpredcl  4672  elvvuni  4740  isarep2  5362  acexmidlemcase  5941  abrexex2  6211  oprabex  6215  oprabrexex2  6217  mpoexw  6301  rdg0  6475  frecex  6482  1on  6511  2on  6513  3on  6515  4on  6516  1onn  6608  2onn  6609  3onn  6610  4onn  6611  mapsnf1o2  6785  exmidpw  7007  exmidpw2en  7011  unfiexmid  7017  xpfi  7031  ssfirab  7035  fnfi  7040  iunfidisj  7050  fidcenumlemr  7059  sbthlemi10  7070  ctmlemr  7212  nninfex  7225  exmidonfinlem  7303  acfun  7321  exmidaclem  7322  pw1ne1  7343  ccfunen  7378  nqex  7478  nq0ex  7555  1pr  7669  ltexprlempr  7723  recexprlempr  7747  cauappcvgprlemcl  7768  caucvgprlemcl  7791  caucvgprprlemcl  7819  addvalex  7959  peano1nnnn  7967  peano2nnnn  7968  axcnex  7974  ax1cn  7976  ax1re  7977  pnfxr  8127  mnfxr  8131  inelr  8659  cju  9036  2re  9108  3re  9112  4re  9115  5re  9117  6re  9119  7re  9121  8re  9123  9re  9125  2nn  9200  3nn  9201  4nn  9202  5nn  9203  6nn  9204  7nn  9205  8nn  9206  9nn  9207  nn0ex  9303  nneoor  9477  zeo  9480  deccl  9520  decnncl  9525  numnncl2  9528  decnncl2  9529  numsucc  9545  numma2c  9551  numadd  9552  numaddc  9553  nummul1c  9554  nummul2c  9555  xnegcl  9956  xrex  9980  ioof  10095  uzennn  10583  xnn0nnen  10584  seqex  10596  m1expcl2  10708  faccl  10882  facwordi  10887  faclbnd2  10889  bccl  10914  lswex  11047  crre  11201  remim  11204  absval  11345  climle  11678  climcvg1nlem  11693  iserabs  11819  geo2lim  11860  prodfclim1  11888  fprodle  11984  ere  12014  ege2le3  12015  eftlub  12034  efsep  12035  tan0  12075  ef01bndlem  12100  nn0o  12251  pczpre  12653  pockthi  12714  igz  12730  ennnfonelemj0  12805  ennnfonelem0  12809  ndxarg  12888  ndxslid  12890  strndxid  12893  basendxnn  12921  strle1g  12971  plusgndxnn  12976  2strbasg  12985  2stropg  12986  tsetndxnn  13054  plendxnn  13068  dsndxnn  13083  unifndxnn  13093  rmodislmodlem  14145  rmodislmod  14146  cndsex  14348  znval  14431  znle  14432  znbaslemnn  14434  znbas  14439  znzrhval  14442  psrval  14461  fczpsrbag  14466  setsmsbasg  14984  cnbl0  15039  cnopncntop  15049  cnopn  15050  remet  15053  divcnap  15070  expcn  15074  climcncf  15089  idcncf  15106  expcncf  15114  cnrehmeocntop  15115  hovercncf  15151  plyrecj  15268  sincn  15274  coscn  15275  2logb9irrALT  15479  2irrexpq  15481  2irrexpqap  15483  lgslem4  15513  lgsdir2lem2  15539  edgfndxnn  15640  bdinex2  15873  bj-inex  15880  012of  15967  2o01f  15968  peano3nninf  15981  cvgcmp2nlemabs  16008  trilpolemisumle  16014