This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )