Theorem sess2

Description: Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	sess2	|- ( A C_ B -> ( R Se B -> R Se A ) )

Proof

Step	Hyp	Ref	Expression
1		ssralv	|- ( A C_ B -> ( A. x e. B { y e. B | y R x } e. _V -> A. x e. A { y e. B | y R x } e. _V ) )
2		rabss2	|- ( A C_ B -> { y e. A | y R x } C_ { y e. B | y R x } )
3		ssexg	|- ( ( { y e. A | y R x } C_ { y e. B | y R x } /\ { y e. B | y R x } e. _V ) -> { y e. A | y R x } e. _V )
4	3	ex	|- ( { y e. A | y R x } C_ { y e. B | y R x } -> ( { y e. B | y R x } e. _V -> { y e. A | y R x } e. _V ) )
5	2 4	syl	|- ( A C_ B -> ( { y e. B | y R x } e. _V -> { y e. A | y R x } e. _V ) )
6	5	ralimdv	|- ( A C_ B -> ( A. x e. A { y e. B | y R x } e. _V -> A. x e. A { y e. A | y R x } e. _V ) )
7	1 6	syld	|- ( A C_ B -> ( A. x e. B { y e. B | y R x } e. _V -> A. x e. A { y e. A | y R x } e. _V ) )
8		df-se	|- ( R Se B <-> A. x e. B { y e. B | y R x } e. _V )
9		df-se	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
10	7 8 9	3imtr4g	|- ( A C_ B -> ( R Se B -> R Se A ) )