Theorem ss2rabdf

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

	Ref	Expression
Hypotheses	ss2rabdf.1	|- F/ x ph
	ss2rabdf.2	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
Assertion	ss2rabdf	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )

Proof

Step	Hyp	Ref	Expression
1		ss2rabdf.1	|- F/ x ph
2		ss2rabdf.2	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ex	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	1 3	ralrimi	|- ( ph -> A. x e. A ( ps -> ch ) )
5		ss2rab	|- ( { x e. A | ps } C_ { x e. A | ch } <-> A. x e. A ( ps -> ch ) )
6	4 5	sylibr	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )