Theorem ssrabdf

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	ssrabdf.1	|- F/_ x A
	ssrabdf.2	|- F/_ x B
	ssrabdf.3	|- F/ x ph
	ssrabdf.4	|- ( ph -> B C_ A )
	ssrabdf.5	|- ( ( ph /\ x e. B ) -> ps )
Assertion	ssrabdf	|- ( ph -> B C_ { x e. A | ps } )

Proof

Step	Hyp	Ref	Expression
1		ssrabdf.1	|- F/_ x A
2		ssrabdf.2	|- F/_ x B
3		ssrabdf.3	|- F/ x ph
4		ssrabdf.4	|- ( ph -> B C_ A )
5		ssrabdf.5	|- ( ( ph /\ x e. B ) -> ps )
6	3 5	ralrimia	|- ( ph -> A. x e. B ps )
7	2 1	ssrabf	|- ( B C_ { x e. A | ps } <-> ( B C_ A /\ A. x e. B ps ) )
8	4 6 7	sylanbrc	|- ( ph -> B C_ { x e. A | ps } )