Theorem sess1

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

	Ref	Expression
Assertion	sess1	|- ( R C_ S -> ( S Se A -> R Se A ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( R C_ S /\ y e. A ) -> R C_ S )
2	1	ssbrd	|- ( ( R C_ S /\ y e. A ) -> ( y R x -> y S x ) )
3	2	ss2rabdv	|- ( R C_ S -> { y e. A | y R x } C_ { y e. A | y S x } )
4		ssexg	|- ( ( { y e. A | y R x } C_ { y e. A | y S x } /\ { y e. A | y S x } e. _V ) -> { y e. A | y R x } e. _V )
5	4	ex	|- ( { y e. A | y R x } C_ { y e. A | y S x } -> ( { y e. A | y S x } e. _V -> { y e. A | y R x } e. _V ) )
6	3 5	syl	|- ( R C_ S -> ( { y e. A | y S x } e. _V -> { y e. A | y R x } e. _V ) )
7	6	ralimdv	|- ( R C_ S -> ( A. x e. A { y e. A | y S x } e. _V -> A. x e. A { y e. A | y R x } e. _V ) )
8		df-se	|- ( S Se A <-> A. x e. A { y e. A | y S 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	|- ( R C_ S -> ( S Se A -> R Se A ) )