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