Theorem eqeltrr 1542

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

Syntax hints:   = wceq 954   e. wcel 956

This theorem is referenced by:  zfrep4 2696  moabex 2761  pp0ex 2766  zfpair 2772  unex 2867  fvresex 3848  abrexex2 3862  abexssex 3863  abexex 3864  oprvalex 4032  pw2en 4432  abfii2 4542  abfii4 4544  inf0 4586  scottexs 4698  kardex 4705  brdom7disj 4784  brdom6disj 4785  cardon 4807  cardid 4808  ondomon 4836  1lt2pi 5012  0cn 5308  0reALT 5421  4nn 5957  om2uzran 6245  unirnioo 6343  sqrlem8 6618  fsump1f 6957  eirrlem5 7342  ef4p 7348  ruclem23 7483  infxpidmlem9 7511  infmap2lem2 7530  gch-kn 7537  subbas 7594  indistop 7598  indistps 7603  distps 7604  issubg 8068  nmofval 8370  ipasslem6 8439  h2hva 8782  h2hsm 8783  h2hnm 8784  norm-ii 8943  shex 9016  hhshsslem2 9077  shincl 9269  chincl 9321  lnophd 9865  bdophd 9968

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain