Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
resexd
Next ⟩
r19.36vf
Metamath Proof Explorer
Ascii
Unicode
Theorem
resexd
Description:
The restriction of a set is a set.
(Contributed by
Glauco Siliprandi
, 23-Oct-2021)
Ref
Expression
Hypothesis
resexd.1
⊢
φ
→
A
∈
V
Assertion
resexd
⊢
φ
→
A
↾
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
resexd.1
⊢
φ
→
A
∈
V
2
resexg
⊢
A
∈
V
→
A
↾
B
∈
V
3
1
2
syl
⊢
φ
→
A
↾
B
∈
V