Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Founded and well-ordering relations
sess1
Next ⟩
sess2
Metamath Proof Explorer
Ascii
Unicode
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