Theorem eqeltr 1542

Description: Substitution of equal classes into membership relation.

Hypotheses

Ref	Expression
eqeltr.1	|- A = B
eqeltr.2	|- B e. C

Assertion

Ref	Expression
eqeltr	|- A e. C

Proof of Theorem eqeltr

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 1535	. 2 |- (A e. C <-> B e. C)
4	1, 3	mpbir 190	1 |- A e. C

Syntax hints:   = wceq 955   e. wcel 957

This theorem is referenced by:  eqeltrr 1543  intab 2556  inex2 2713  zfpair 2773  opex 2778  uniopel 2805  unisn2 2871  tpex 2874  elvvuni 3225  isarep2 3574  fopabex2 3608  fvex 3727  abrexexlem2 3854  abrexex2 3866  oprex 3978  oprabex 4014  1on 4131  oesuc 4159  oecl 4165  nnecl 4224  1onn 4246  2onn 4247  supex 4560  inf0 4589  oancom 4616  rankr1 4657  hta 4711  aceq5lem4 4721  aceq5lem5 4722  ac6lem 4737  kmlem10 4757  brdom7disj 4787  brdom6disj 4788  cardon 4810  cardid 4811  alephon 4848  alephfplem1 4879  nqex 5032  srex 5162  axcnex 5250  ax1cn 5252  negex 5348  subcl 5349  xrex 5475  pnfxr 5476  mnfxr 5477  pnfnemnf 5519  divcl 5689  redivcl 5764  nnsub 5913  2re 5936  3re 5938  4re 5939  5re 5940  6re 5941  7re 5942  8re 5943  9re 5944  10re 5945  2nn 5956  3nn 5957  nneo 6154  zeot 6156  om2uzuz 6247  ser1recl 6281  ser0cl1 6509  discrlem1 6601  sqrlem7 6624  inelr 6680  facclt 6892  facwordit 6896  faclbnd2 6898  bccl2t 6924  sumex 6934  iserzshft 7097  iserzabslem 7131  cvgcmp2lem 7133  isumshft 7156  isumshft2 7157  infcvglem1 7173  infcvglem2 7174  infcvglem3 7175  ivthlem5 7237  isupivth 7242  ivthlem5OLD 7246  reefcl 7276  erelem7 7284  ere 7289  efaddlem7 7303  efaddlem8 7304  efaddlem21 7317  ef1tllem 7340  absef01tlub 7346  eirrlem2 7348  efcnlem2 7377  sin01bndlem1 7426  sin01bndlem2 7427  cos01bndlem2 7429  ruclem5 7474  ruclem13 7482  ruclem15 7484  ruclem34 7503  infxpidmlem8 7519  infxpidmlem9 7520  infmap2lem2 7540  indistop 7608  fctop2 7611  lpval 7703  ismsi 7761  metxp 7796  opntop 7832  cncfmet 7867  remet 7872  rehaus 7879  lmfex 7921  fsumcnlem 7951  bcthlem12 7972  bcthlem15 7975  bcthlem30 7990  issubg 8080  issubgi 8086  ghgrpilem4 8100  isvci 8165  isnvi 8196  imsval 8280  imsmetlem 8287  ipfval 8314  sspval 8344  lnoval 8375  islno 8376  nmofval 8385  nmoval 8386  bloval 8401  0ofval 8407  0oval 8408  blocni 8424  ajfval 8428  hmoval 8429  cnph 8437  isph 8440  phpar 8442  ipasslem7 8455  siilem2 8471  ubthlem1 8488  ubthlem6 8493  minveclem12 8515  minveccl 8543  hlex 8558  htthlem11 8588  sincn 8623  coscn 8624  pilem3 8627  circgrpOLD 8693  pilog 8723  normlem2 8932  normlem3 8933  normlem6 8936  shex 9032  h0elch 9082  hhsssh 9094  projlem11 9151  pjthlem1 9174  pjthlem9 9182  pjthlem10 9183  pjthlem11 9184  pjthlem12 9185  pjthlem13 9186  pjthlem14 9187  spansnj 9548  nonbool 9553  3oalem5 9568  3oalem6 9569  3oa 9570  nmbdfnlbt 9935  cnlnadjlem5 9960  pjbdln 10032  golem2 10155  goeq 10156  ghomgrpilem2 10342  ghomsn 10344  ghomgrplem 10345  cayleylem1 10365  cayleylem2 10366  cayleylem3 10367  cayleythlem 10369  hmeogrp 10484  subsp 10488  limfillem1 10523  dtopcl 10531  stoi 10555  ishomb 10632  ismona 10651  isfuna 10664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1468  df-clel 1471

Copyright terms: Public domain