Metamath Proof Explorer


Theorem resexd

Description: The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis resexd.1 ( 𝜑𝐴𝑉 )
Assertion resexd ( 𝜑 → ( 𝐴𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 resexd.1 ( 𝜑𝐴𝑉 )
2 resexg ( 𝐴𝑉 → ( 𝐴𝐵 ) ∈ V )
3 1 2 syl ( 𝜑 → ( 𝐴𝐵 ) ∈ V )