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

Metamath Proof Explorer

Theorem ssrd

Description: Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypotheses ssrd.0 ⊢ Ⅎ x φ
ssrd.1 ⊢ Ⅎ _ x A
ssrd.2 ⊢ Ⅎ _ x B
ssrd.3 ⊢ φ → x ∈ A → x ∈ B
Assertion ssrd ⊢ φ → A ⊆ B

Proof

Step Hyp Ref Expression
1 ssrd.0 ⊢ Ⅎ x φ
2 ssrd.1 ⊢ Ⅎ _ x A
3 ssrd.2 ⊢ Ⅎ _ x B
4 ssrd.3 ⊢ φ → x ∈ A → x ∈ B
5 1 4 alrimi ⊢ φ → ∀ x x ∈ A → x ∈ B
6 2 3 dfssf ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B
7 5 6 sylibr ⊢ φ → A ⊆ B