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	|- A. x e. ~P x x e. _V

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	rgenw	|- A. x e. ~P x x e. _V