Theorem ssrd

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

	Ref	Expression
Hypotheses	ssrd.0	⊢ Ⅎ 𝑥 𝜑
	ssrd.1	⊢ Ⅎ 𝑥 𝐴
	ssrd.2	⊢ Ⅎ 𝑥 𝐵
	ssrd.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
Assertion	ssrd	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssrd.0	⊢ Ⅎ 𝑥 𝜑
2		ssrd.1	⊢ Ⅎ 𝑥 𝐴
3		ssrd.2	⊢ Ⅎ 𝑥 𝐵
4		ssrd.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
5	1 4	alrimi	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6	2 3	dfss2f	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
7	5 6	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )