Theorem ssdf2

Description: A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	ssdf2.p	|- F/ x ph
	ssdf2.a	|- F/_ x A
	ssdf2.b	|- F/_ x B
	ssdf2.x	|- ( ( ph /\ x e. A ) -> x e. B )
Assertion	ssdf2	|- ( ph -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		ssdf2.p	|- F/ x ph
2		ssdf2.a	|- F/_ x A
3		ssdf2.b	|- F/_ x B
4		ssdf2.x	|- ( ( ph /\ x e. A ) -> x e. B )
5	4	ex	|- ( ph -> ( x e. A -> x e. B ) )
6	1 2 3 5	ssrd	|- ( ph -> A C_ B )