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	⊢ ∀ 𝑥 ∈ 𝒫 𝑥 𝑥 ∈ V

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	rgenw	⊢ ∀ 𝑥 ∈ 𝒫 𝑥 𝑥 ∈ V