Theorem eqeltrr 1548

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 1482	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltr 1547	1 |- B e. C

Syntax hints:   = wceq 958   e. wcel 960

This theorem is referenced by:  zfrep4 2706  moabex 2772  pp0ex 2777  zfpair 2783  unex 2878  fvresex 3863  abrexex2 3877  abexssex 3878  abexex 3879  oprvalex 4047  pw2en 4452  inf0 4615  scottexs 4728  kardex 4735  brdom7disj 4814  brdom6disj 4815  cardon 4837  cardid 4838  ondomon 4867  1lt2pi 5044  0cn 5340  0reALT 5453  4nn 6004  om2uzran 6301  unirnioo 6403  sqrlem8 6681  fsump1f 7011  eirrlem5 7393  ef4p 7399  ruclem23 7533  infxpidmlem9 7561  infmap2lem2 7582  gch-kn 7589  indistop 7645  indistps 7650  distps 7651  issubg 8112  nmofval 8421  ipasslem6 8491  h2hva 8838  h2hsm 8839  h2hnm 8840  norm-ii 8999  shex 9072  hhshsslem2 9133  shincl 9326  chincl 9378  lnophd 9922  bdophd 10025

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain