Theorem ssdf

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

	Ref	Expression
Hypotheses	ssdf.1	|- F/ x ph
	ssdf.2	|- ( ( ph /\ x e. A ) -> x e. B )
Assertion	ssdf	|- ( ph -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		ssdf.1	|- F/ x ph
2		ssdf.2	|- ( ( ph /\ x e. A ) -> x e. B )
3	2	ex	|- ( ph -> ( x e. A -> x e. B ) )
4	1 3	ralrimi	|- ( ph -> A. x e. A x e. B )
5		dfss3	|- ( A C_ B <-> A. x e. A x e. B )
6	4 5	sylibr	|- ( ph -> A C_ B )