Metamath Proof Explorer


Theorem elpwi2OLD

Description: Obsolete version of elpwi2 as of 26-May-2024. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses elpwi2.1 B V
elpwi2.2 A B
Assertion elpwi2OLD A 𝒫 B

Proof

Step Hyp Ref Expression
1 elpwi2.1 B V
2 elpwi2.2 A B
3 elpw2g B V A 𝒫 B A B
4 1 3 ax-mp A 𝒫 B A B
5 2 4 mpbir A 𝒫 B