Theorem eqeltri 2269

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

Syntax hints:   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrri  2270  3eltr4i  2278  intab  3904  inex2  4169  vpwex  4213  ord3ex  4224  uniopel  4290  onsucelsucexmid  4567  nnpredcl  4660  elvvuni  4728  isarep2  5346  acexmidlemcase  5920  abrexex2  6190  oprabex  6194  oprabrexex2  6196  mpoexw  6280  rdg0  6454  frecex  6461  1on  6490  2on  6492  3on  6494  4on  6495  1onn  6587  2onn  6588  3onn  6589  4onn  6590  mapsnf1o2  6764  exmidpw  6978  exmidpw2en  6982  unfiexmid  6988  xpfi  7002  ssfirab  7006  fnfi  7011  iunfidisj  7021  fidcenumlemr  7030  sbthlemi10  7041  ctmlemr  7183  nninfex  7196  exmidonfinlem  7272  acfun  7290  exmidaclem  7291  pw1ne1  7312  ccfunen  7347  nqex  7447  nq0ex  7524  1pr  7638  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  caucvgprlemcl  7760  caucvgprprlemcl  7788  addvalex  7928  peano1nnnn  7936  peano2nnnn  7937  axcnex  7943  ax1cn  7945  ax1re  7946  pnfxr  8096  mnfxr  8100  inelr  8628  cju  9005  2re  9077  3re  9081  4re  9084  5re  9086  6re  9088  7re  9090  8re  9092  9re  9094  2nn  9169  3nn  9170  4nn  9171  5nn  9172  6nn  9173  7nn  9174  8nn  9175  9nn  9176  nn0ex  9272  nneoor  9445  zeo  9448  deccl  9488  decnncl  9493  numnncl2  9496  decnncl2  9497  numsucc  9513  numma2c  9519  numadd  9520  numaddc  9521  nummul1c  9522  nummul2c  9523  xnegcl  9924  xrex  9948  ioof  10063  uzennn  10545  xnn0nnen  10546  seqex  10558  m1expcl2  10670  faccl  10844  facwordi  10849  faclbnd2  10851  bccl  10876  crre  11039  remim  11042  absval  11183  climle  11516  climcvg1nlem  11531  iserabs  11657  geo2lim  11698  prodfclim1  11726  fprodle  11822  ere  11852  ege2le3  11853  eftlub  11872  efsep  11873  tan0  11913  ef01bndlem  11938  nn0o  12089  pczpre  12491  pockthi  12552  igz  12568  ennnfonelemj0  12643  ennnfonelem0  12647  ndxarg  12726  ndxslid  12728  strndxid  12731  basendxnn  12759  strle1g  12809  plusgndxnn  12814  2strbasg  12822  2stropg  12823  tsetndxnn  12891  plendxnn  12905  dsndxnn  12920  unifndxnn  12930  rmodislmodlem  13982  rmodislmod  13983  cndsex  14185  znval  14268  znle  14269  znbaslemnn  14271  znbas  14276  znzrhval  14279  psrval  14296  fczpsrbag  14301  setsmsbasg  14799  cnbl0  14854  cnopncntop  14864  cnopn  14865  remet  14868  divcnap  14885  expcn  14889  climcncf  14904  idcncf  14921  expcncf  14929  cnrehmeocntop  14930  hovercncf  14966  plyrecj  15083  sincn  15089  coscn  15090  2logb9irrALT  15294  2irrexpq  15296  2irrexpqap  15298  lgslem4  15328  lgsdir2lem2  15354  bdinex2  15630  bj-inex  15637  012of  15724  2o01f  15725  peano3nninf  15738  cvgcmp2nlemabs  15763  trilpolemisumle  15769