Theorem enmappwid

Description: The set of all mappings from the powerset to the powerset is equinumerous to the set of all mappings from the set to the powerset of the powerset. (Contributed by RP, 27-Apr-2021)

	Ref	Expression
Assertion	enmappwid	|- ( A e. V -> ( ~P A ^m ~P A ) ~~ ( ~P ~P A ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		pwexg	|- ( A e. V -> ~P A e. _V )
2		enmappw	|- ( ( ~P A e. _V /\ A e. V ) -> ( ~P A ^m ~P A ) ~~ ( ~P ~P A ^m A ) )
3	1 2	mpancom	|- ( A e. V -> ( ~P A ^m ~P A ) ~~ ( ~P ~P A ^m A ) )