Theorem eqeltrr 1545

Description: Substitution of equal classes into membership relation.

Hypotheses

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

Assertion

Ref	Expression
eqeltrr	|- B e. C

Proof of Theorem eqeltrr

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 |- A = B
2	1	eqcomi 1479	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltr 1544	1 |- B e. C

Syntax hints:   = wceq 956   e. wcel 958

This theorem is referenced by:  zfrep4 2701  moabex 2766  pp0ex 2771  zfpair 2777  unex 2872  fvresex 3857  abrexex2 3871  abexssex 3872  abexex 3873  oprvalex 4041  pw2en 4446  abfii2OLD 4562  abfii4OLD 4564  inf0 4606  scottexs 4718  kardex 4725  brdom7disj 4804  brdom6disj 4805  cardon 4827  cardid 4828  ondomon 4856  1lt2pi 5032  0cn 5328  0reALT 5441  4nn 6002  om2uzran 6300  unirnioo 6402  sqrlem8 6680  fsump1f 7011  eirrlem5 7393  ef4p 7399  ruclem23 7532  infxpidmlem9 7560  infmap2lem2 7580  gch-kn 7587  subbasOLD 7644  indistop 7648  indistps 7653  distps 7654  issubg 8116  nmofval 8425  ipasslem6 8495  h2hva 8843  h2hsm 8844  h2hnm 8845  norm-ii 9004  shex 9077  hhshsslem2 9138  shincl 9331  chincl 9383  lnophd 9927  bdophd 10030

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain