Theorem elpwi2

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof shortened by Wolf Lammen, 26-May-2024)

	Ref	Expression
Hypotheses	elpwi2.1	|- B e. V
	elpwi2.2	|- A C_ B
Assertion	elpwi2	|- A e. ~P B

Proof

Step	Hyp	Ref	Expression
1		elpwi2.1	|- B e. V
2		elpwi2.2	|- A C_ B
3	1	elexi	|- B e. _V
4	3	elpw2	|- ( A e. ~P B <-> A C_ B )
5	2 4	mpbir	|- A e. ~P B