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	1 2	ralrimia	|- ( ph -> A. x e. A ( ps -> ch ) )
4	3	ss2rabd	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )