Theorem eqeltri 2227

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

Syntax hints:   = wceq 1332   e. wcel 2125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147  df-clel 2150

This theorem is referenced by:  eqeltrri  2228  3eltr4i  2236  intab  3832  inex2  4095  vpwex  4135  ord3ex  4146  uniopel  4211  onsucelsucexmid  4483  nnpredcl  4576  elvvuni  4643  isarep2  5250  acexmidlemcase  5809  abrexex2  6062  oprabex  6066  oprabrexex2  6068  rdg0  6324  frecex  6331  1on  6360  2on  6362  3on  6364  4on  6365  1onn  6456  2onn  6457  3onn  6458  4onn  6459  mapsnf1o2  6630  exmidpw  6842  unfiexmid  6851  xpfi  6863  ssfirab  6867  fnfi  6870  iunfidisj  6879  fidcenumlemr  6888  sbthlemi10  6899  ctmlemr  7038  nninfex  7051  exmidonfinlem  7107  acfun  7121  exmidaclem  7122  pw1ne1  7143  ccfunen  7163  nqex  7262  nq0ex  7339  1pr  7453  ltexprlempr  7507  recexprlempr  7531  cauappcvgprlemcl  7552  caucvgprlemcl  7575  caucvgprprlemcl  7603  addvalex  7743  peano1nnnn  7751  peano2nnnn  7752  axcnex  7758  ax1cn  7760  ax1re  7761  pnfxr  7909  mnfxr  7913  inelr  8438  cju  8811  2re  8882  3re  8886  4re  8889  5re  8891  6re  8893  7re  8895  8re  8897  9re  8899  2nn  8973  3nn  8974  4nn  8975  5nn  8976  6nn  8977  7nn  8978  8nn  8979  9nn  8980  nn0ex  9075  nneoor  9245  zeo  9248  deccl  9288  decnncl  9293  numnncl2  9296  decnncl2  9297  numsucc  9313  numma2c  9319  numadd  9320  numaddc  9321  nummul1c  9322  nummul2c  9323  xnegcl  9714  xrex  9738  ioof  9853  uzennn  10313  seqex  10324  m1expcl2  10419  faccl  10586  facwordi  10591  faclbnd2  10593  bccl  10618  crre  10734  remim  10737  absval  10878  climle  11208  climcvg1nlem  11223  iserabs  11349  geo2lim  11390  prodfclim1  11418  fprodle  11514  ere  11544  ege2le3  11545  eftlub  11564  efsep  11565  tan0  11605  ef01bndlem  11630  nn0o  11771  ennnfonelemj0  12081  ennnfonelem0  12085  ndxarg  12152  ndxslid  12154  strndxid  12157  basendxnn  12184  strle1g  12219  2strbasg  12230  2stropg  12231  setsmsbasg  12818  cnbl0  12873  cnopncntop  12876  remet  12879  divcnap  12894  climcncf  12910  expcncf  12931  cnrehmeocntop  12932  sincn  13029  coscn  13030  2logb9irrALT  13230  2irrexpq  13232  2irrexpqap  13234  bdinex2  13413  bj-inex  13420  012of  13506  2o01f  13507  peano3nninf  13519  cvgcmp2nlemabs  13544  trilpolemisumle  13550