Theorem rabssd

Description: Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	rabssd.1	⊢ Ⅎ 𝑥 𝜑
	rabssd.2	⊢ Ⅎ 𝑥 𝐵
	rabssd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 ) → 𝑥 ∈ 𝐵 )
Assertion	rabssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜒 } ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rabssd.1	⊢ Ⅎ 𝑥 𝜑
2		rabssd.2	⊢ Ⅎ 𝑥 𝐵
3		rabssd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 ) → 𝑥 ∈ 𝐵 )
4	3	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜒 → 𝑥 ∈ 𝐵 ) ) )
5	1 4	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜒 → 𝑥 ∈ 𝐵 ) )
6	2	rabssf	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜒 } ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜒 → 𝑥 ∈ 𝐵 ) )
7	5 6	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜒 } ⊆ 𝐵 )