Theorem ss2rabdf

Description: Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	ss2rabdf.1	$$⊢Ⅎx\phi$$
	ss2rabdf.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \to \chi \right)$$
Assertion	ss2rabdf	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in A|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ss2rabdf.1	$$⊢Ⅎx\phi$$
2		ss2rabdf.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \to \chi \right)$$
3	1 2	ralrimia	$$⊢\phi \to \forall x\in A\left(\psi \to \chi \right)$$
4	3	ss2rabd	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in A|\chi \right\}$$