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 S S Se A R Se A

Proof

Step Hyp Ref Expression
1 simpl R S y A R S
2 1 ssbrd R S y A y R x y S x
3 2 ss2rabdv R S y A | y R x y A | y S x
4 ssexg y A | y R x y A | y S x y A | y S x V y A | y R x V
5 4 ex y A | y R x y A | y S x y A | y S x V y A | y R x V
6 3 5 syl R S y A | y S x V y A | y R x V
7 6 ralimdv R S x A y A | y S x V x A y A | y R x V
8 df-se S Se A x A y A | y S x V
9 df-se R Se A x A y A | y R x V
10 7 8 9 3imtr4g R S S Se A R Se A