Metamath Proof Explorer

Theorem sbcssg

Description: Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012) (Proof shortened by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion sbcssg ⊢A∈V→[˙A/x]˙B⊆C↔⦋A/x⦌B⊆⦋A/x⦌C

Proof

Step Hyp Ref Expression
1 sbcal ⊢[˙A/x]˙∀yy∈B→y∈C↔∀y[˙A/x]˙y∈B→y∈C
2 sbcimg ⊢A∈V→[˙A/x]˙y∈B→y∈C↔[˙A/x]˙y∈B→[˙A/x]˙y∈C
3 sbcel2 ⊢[˙A/x]˙y∈B↔y∈⦋A/x⦌B
4 sbcel2 ⊢[˙A/x]˙y∈C↔y∈⦋A/x⦌C
5 3 4 imbi12i ⊢[˙A/x]˙y∈B→[˙A/x]˙y∈C↔y∈⦋A/x⦌B→y∈⦋A/x⦌C
6 2 5 bitrdi ⊢A∈V→[˙A/x]˙y∈B→y∈C↔y∈⦋A/x⦌B→y∈⦋A/x⦌C
7 6 albidv ⊢A∈V→∀y[˙A/x]˙y∈B→y∈C↔∀yy∈⦋A/x⦌B→y∈⦋A/x⦌C
8 1 7 bitrid ⊢A∈V→[˙A/x]˙∀yy∈B→y∈C↔∀yy∈⦋A/x⦌B→y∈⦋A/x⦌C
9 dfss2 ⊢B⊆C↔∀yy∈B→y∈C
10 9 sbcbii ⊢[˙A/x]˙B⊆C↔[˙A/x]˙∀yy∈B→y∈C
11 dfss2 ⊢⦋A/x⦌B⊆⦋A/x⦌C↔∀yy∈⦋A/x⦌B→y∈⦋A/x⦌C
12 8 10 11 3bitr4g ⊢A∈V→[˙A/x]˙B⊆C↔⦋A/x⦌B⊆⦋A/x⦌C