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

Metamath Proof Explorer

Theorem ssdf2

Description: A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses ssdf2.p ⊢ Ⅎ x φ
ssdf2.a ⊢ Ⅎ _ x A
ssdf2.b ⊢ Ⅎ _ x B
ssdf2.x ⊢ φ ∧ x ∈ A → x ∈ B
Assertion ssdf2 ⊢ φ → A ⊆ B

Proof

Step Hyp Ref Expression
1 ssdf2.p ⊢ Ⅎ x φ
2 ssdf2.a ⊢ Ⅎ _ x A
3 ssdf2.b ⊢ Ⅎ _ x B
4 ssdf2.x ⊢ φ ∧ x ∈ A → x ∈ B
5 4 ex ⊢ φ → x ∈ A → x ∈ B
6 1 2 3 5 ssrd ⊢ φ → A ⊆ B