Metamath Proof Explorer


Theorem pwidgOLD

Description: Obsolete version of pwidg as of 10-Jun-2026. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwidgOLD A V A 𝒫 A

Proof

Step Hyp Ref Expression
1 ssid A A
2 elpwg A V A 𝒫 A A A
3 1 2 mpbiri A V A 𝒫 A