Theorem ssdf

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

	Ref	Expression
Hypotheses	ssdf.1	⊢ Ⅎ 𝑥 𝜑
	ssdf.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
Assertion	ssdf	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssdf.1	⊢ Ⅎ 𝑥 𝜑
2		ssdf.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
3	2	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
4	1 3	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
5		dfss3	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
6	4 5	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )