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	2	ex	$$⊢\phi \to \left(x\in A\to \left(\psi \to \chi \right)\right)$$
4	1 3	ralrimi	$$⊢\phi \to \forall x\in A\left(\psi \to \chi \right)$$
5		ss2rab	$$⊢\left\{x\in A|\psi \right\}\subseteq \left\{x\in A|\chi \right\}\leftrightarrow \forall x\in A\left(\psi \to \chi \right)$$
6	4 5	sylibr	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq \left\{x\in A|\chi \right\}$$