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	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )