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 ⊢ Ⅎ 𝑥 𝜑
ssdf2.a ⊢ Ⅎ 𝑥 𝐴
ssdf2.b ⊢ Ⅎ 𝑥 𝐵
ssdf2.x ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
Assertion ssdf2 ( 𝜑 → 𝐴 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 ssdf2.p ⊢ Ⅎ 𝑥 𝜑
2 ssdf2.a ⊢ Ⅎ 𝑥 𝐴
3 ssdf2.b ⊢ Ⅎ 𝑥 𝐵
4 ssdf2.x ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
5 4 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6 1 2 3 5 ssrd ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )