Metamath Proof Explorer

Theorem sess2

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

Ref Expression
Assertion sess2 ⊢ A ⊆ B → R Se B → R Se A

Proof

Step Hyp Ref Expression
1 ssralv ⊢ A ⊆ B → ∀ x ∈ B y ∈ B | y R x ∈ V → ∀ x ∈ A y ∈ B | y R x ∈ V
2 rabss2 ⊢ A ⊆ B → y ∈ A | y R x ⊆ y ∈ B | y R x
3 ssexg ⊢ y ∈ A | y R x ⊆ y ∈ B | y R x ∧ y ∈ B | y R x ∈ V → y ∈ A | y R x ∈ V
4 3 ex ⊢ y ∈ A | y R x ⊆ y ∈ B | y R x → y ∈ B | y R x ∈ V → y ∈ A | y R x ∈ V
5 2 4 syl ⊢ A ⊆ B → y ∈ B | y R x ∈ V → y ∈ A | y R x ∈ V
6 5 ralimdv ⊢ A ⊆ B → ∀ x ∈ A y ∈ B | y R x ∈ V → ∀ x ∈ A y ∈ A | y R x ∈ V
7 1 6 syld ⊢ A ⊆ B → ∀ x ∈ B y ∈ B | y R x ∈ V → ∀ x ∈ A y ∈ A | y R x ∈ V
8 df-se ⊢ R Se B ↔ ∀ x ∈ B y ∈ B | y R x ∈ V
9 df-se ⊢ R Se A ↔ ∀ x ∈ A y ∈ A | y R x ∈ V
10 7 8 9 3imtr4g ⊢ A ⊆ B → R Se B → R Se A