Theorem ssrel3

Description: Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019)

	Ref	Expression
Assertion	ssrel3	|- ( Rel A -> ( A C_ B <-> A. x A. y ( x A y -> x B y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssrel	|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
2		df-br	|- ( x A y <-> <. x , y >. e. A )
3		df-br	|- ( x B y <-> <. x , y >. e. B )
4	2 3	imbi12i	|- ( ( x A y -> x B y ) <-> ( <. x , y >. e. A -> <. x , y >. e. B ) )
5	4	2albii	|- ( A. x A. y ( x A y -> x B y ) <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
6	1 5	bitr4di	|- ( Rel A -> ( A C_ B <-> A. x A. y ( x A y -> x B y ) ) )