Theorem eqeltrr 1160

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

Syntax hints:   = wceq 1091   e. wcel 1092

This theorem is referenced by:  zfrep4 1479  0ex 1745  moabex 1868  pp0ex 1886  zfpair 1891  unex 1949  fvresex 2909  abrexex2 2915  oprvalex 3055  pw2en 3348  inf0 3457  scottexs 3543  kardex 3550  cardon 3634  cardid 3635  ondomon 3662  1lt2pi 3826  om2uzran 4655  sqrlem8 4738  ruclem23 4907  infxpidmlem9 4941  infmap2lem2 4952  gch-kn 4957  norm-ii 5086  shex 5115  shincl 5332  chincl 5382

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