Metamath Proof Explorer

Theorem exrecfnpw

Description: For any base set, a set which contains the powerset of all of its own elements exists. (Contributed by ML, 30-Mar-2022)

Ref Expression
Assertion exrecfnpw 
|- ( A e. V -> E. x ( A C_ x /\ A. y e. x ~P y e. x ) )

Proof

Step Hyp Ref Expression
1 vpwex 
 |-  ~P y e. _V
2 1 ax-gen 
 |-  A. y ~P y e. _V
3 exrecfn 
 |-  ( ( A e. V /\ A. y ~P y e. _V ) -> E. x ( A C_ x /\ A. y e. x ~P y e. x ) )
4 2 3 mpan2 
 |-  ( A e. V -> E. x ( A C_ x /\ A. y e. x ~P y e. x ) )