Metamath Proof Explorer


Theorem ralndv2

Description: Second example for a theorem about a restricted universal quantification in which the restricting class depends on the bound variable: all subsets of a set are sets. (Contributed by AV, 24-Jun-2023)

Ref Expression
Assertion ralndv2 x 𝒫 x x V

Proof

Step Hyp Ref Expression
1 vex x V
2 1 rgenw x 𝒫 x x V