Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
3sstr4g
Metamath Proof Explorer
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
$${\u22a2}{\phi}\to {A}\subseteq {B}$$
3sstr4g.2
$${\u22a2}{C}={A}$$
3sstr4g.3
$${\u22a2}{D}={B}$$
Assertion
3sstr4g
$${\u22a2}{\phi}\to {C}\subseteq {D}$$

Proof
Step
Hyp
Ref
Expression
1
3sstr4g.1
$${\u22a2}{\phi}\to {A}\subseteq {B}$$
2
3sstr4g.2
$${\u22a2}{C}={A}$$
3
3sstr4g.3
$${\u22a2}{D}={B}$$
4
2 3
sseq12i
$${\u22a2}{C}\subseteq {D}\leftrightarrow {A}\subseteq {B}$$
5
1 4
sylibr
$${\u22a2}{\phi}\to {C}\subseteq {D}$$