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 3sstr4d
Description: Substitution of equality into both sides of a subclass relationship.
(Contributed by NM , 30-Nov-1995) (Proof shortened by Eric Schmidt , 26-Jan-2007)
Ref
Expression
Hypotheses
3sstr4d.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3sstr4d.2 ⊢ ( 𝜑 → 𝐶 = 𝐴 )
3sstr4d.3 ⊢ ( 𝜑 → 𝐷 = 𝐵 )
Assertion
3sstr4d ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
Proof
Step
Hyp
Ref
Expression
1
3sstr4d.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2
3sstr4d.2 ⊢ ( 𝜑 → 𝐶 = 𝐴 )
3
3sstr4d.3 ⊢ ( 𝜑 → 𝐷 = 𝐵 )
4
2 1
eqsstrd ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
5
4 3
sseqtrrd ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )