Theorem eqeltr 1159

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

Syntax hints:   = wceq 1091   e. wcel 1092

This theorem is referenced by:  eqeltrr 1160  inex2 1698  zfpair 1891  opex 1893  tpex 1952  supex 2157  fvex 2838  abrexexlem2 2911  iunex 2914  abrexex2 2915  oprex 3018  oprabex 3044  1o 3109  oesuc 3134  oecl 3140  1onn 3193  2onn 3194  qsex 3231  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  inf0 3457  rankr1 3518  aceq5lem4 3561  aceq5lem5 3562  ac6lem 3575  kmlem9 3588  hta 3619  cardon 3634  cardid 3635  alephon 3671  nqex 3843  srex 3973  axcnex 4061  ax0re 4063  ax1re 4064  subcl 4139  divcl 4221  redivcl 4274  nnsub 4450  2re 4470  3re 4472  4re 4473  5re 4474  6re 4475  7re 4476  8re 4477  9re 4478  2nn 4487  inelr 4527  om2uzuz 4653  discrlem1 4713  nnsqcl 4717  nneo 4719  sqrlem7 4737  abscl 4840  facclt 4874  ruclem5 4889  ruclem13 4897  ruclem15 4899  infxpidmlem8 4940  infxpidmlem9 4941  infmap2lem2 4952  normlem2 5064  normlem3 5065  normlem6 5068  shex 5115  h0elch 5159  occllem6 5185  projlem11 5203  projlem25 5217  projlem26 5218  pjthlem1 5225  pjthlem9 5233  pjthlem10 5234  pjthlem11 5235  pjthlem12 5236  pjthlem13 5237  pjthlem14 5238  spansnj 5539  3oalem5 5556  3oalem6 5557  3oa 5558  pjoi0 5592  golem2 5705  goeq 5706

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org