This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Subclasses and subsets 3sstr4g
Description: Substitution of equality into both sides of a subclass relationship.
(Contributed by NM , 16-Aug-1994) (Proof shortened by Eric Schmidt , 26-Jan-2007)
Ref
Expression
Hypotheses
3sstr4g.1 |- ( ph -> A C_ B )
3sstr4g.2 |- C = A
3sstr4g.3 |- D = B
Assertion
3sstr4g |- ( ph -> C C_ D )
Proof
Step
Hyp
Ref
Expression
1
3sstr4g.1 |- ( ph -> A C_ B )
2
3sstr4g.2 |- C = A
3
3sstr4g.3 |- D = B
4
2 1
eqsstrid |- ( ph -> C C_ B )
5
4 3
sseqtrrdi |- ( ph -> C C_ D )