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	$$⊢\forall x\in 𝒫xx\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	rgenw	$$⊢\forall x\in 𝒫xx\in \mathrm{V}$$