Theorem relssdv

Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004)

	Ref	Expression
Hypotheses	relssdv.1	|- ( ph -> Rel A )
	relssdv.2	|- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
Assertion	relssdv	|- ( ph -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		relssdv.1	|- ( ph -> Rel A )
2		relssdv.2	|- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
3	2	alrimivv	|- ( ph -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
4		ssrel	|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
5	1 4	syl	|- ( ph -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
6	3 5	mpbird	|- ( ph -> A C_ B )