Theorem ssrd

Description: Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypotheses	ssrd.0	|- F/ x ph
	ssrd.1	|- F/_ x A
	ssrd.2	|- F/_ x B
	ssrd.3	|- ( ph -> ( x e. A -> x e. B ) )
Assertion	ssrd	|- ( ph -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		ssrd.0	|- F/ x ph
2		ssrd.1	|- F/_ x A
3		ssrd.2	|- F/_ x B
4		ssrd.3	|- ( ph -> ( x e. A -> x e. B ) )
5	1 4	alrimi	|- ( ph -> A. x ( x e. A -> x e. B ) )
6	2 3	dfss2f	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
7	5 6	sylibr	|- ( ph -> A C_ B )