This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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]˙ ∀ y y ∈ 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 ↔ ∀ y y ∈ ⦋ A / x⦌ B → y ∈ ⦋ A / x⦌ C
8 1 7 bitrid ⊢ A ∈ V → [˙A / x]˙ ∀ y y ∈ B → y ∈ C ↔ ∀ y y ∈ ⦋ A / x⦌ B → y ∈ ⦋ A / x⦌ C
9 df-ss ⊢ B ⊆ C ↔ ∀ y y ∈ B → y ∈ C
10 9 sbcbii ⊢ [˙A / x]˙ B ⊆ C ↔ [˙A / x]˙ ∀ y y ∈ B → y ∈ C
11 df-ss ⊢ ⦋ A / x⦌ B ⊆ ⦋ A / x⦌ C ↔ ∀ y y ∈ ⦋ A / x⦌ B → y ∈ ⦋ A / x⦌ C
12 8 10 11 3bitr4g ⊢ A ∈ V → [˙A / x]˙ B ⊆ C ↔ ⦋ A / x⦌ B ⊆ ⦋ A / x⦌ C