Theorem elpwgded

Description: elpwgdedVD in conventional notation. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elpwgded.1	|- ( ph -> A e. _V )
	elpwgded.2	|- ( ps -> A C_ B )
Assertion	elpwgded	|- ( ( ph /\ ps ) -> A e. ~P B )

Proof

Step	Hyp	Ref	Expression
1		elpwgded.1	|- ( ph -> A e. _V )
2		elpwgded.2	|- ( ps -> A C_ B )
3		elpwg	|- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimpar	|- ( ( A e. _V /\ A C_ B ) -> A e. ~P B )
5	1 2 4	syl2an	|- ( ( ph /\ ps ) -> A e. ~P B )