Theorem pwnex

Description: The class of all power sets is a proper class. See also snnex . (Contributed by BJ, 2-May-2021)

	Ref	Expression
Assertion	pwnex	|- { x | E. y x = ~P y } e/ _V

Proof

Step	Hyp	Ref	Expression
1		abnex	|- ( A. y ( ~P y e. _V /\ y e. ~P y ) -> -. { x | E. y x = ~P y } e. _V )
2		df-nel	|- ( { x | E. y x = ~P y } e/ _V <-> -. { x | E. y x = ~P y } e. _V )
3	1 2	sylibr	|- ( A. y ( ~P y e. _V /\ y e. ~P y ) -> { x | E. y x = ~P y } e/ _V )
4		vpwex	|- ~P y e. _V
5		vex	|- y e. _V
6	5	pwid	|- y e. ~P y
7	4 6	pm3.2i	|- ( ~P y e. _V /\ y e. ~P y )
8	3 7	mpg	|- { x | E. y x = ~P y } e/ _V