Theorem dfon2lem2

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)

	Ref	Expression
Assertion	dfon2lem2	|- U. { x | ( x C_ A /\ ph /\ ps ) } C_ A

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( x C_ A /\ ph /\ ps ) -> x C_ A )
2	1	ss2abi	|- { x | ( x C_ A /\ ph /\ ps ) } C_ { x | x C_ A }
3		df-pw	|- ~P A = { x | x C_ A }
4	2 3	sseqtrri	|- { x | ( x C_ A /\ ph /\ ps ) } C_ ~P A
5		sspwuni	|- ( { x | ( x C_ A /\ ph /\ ps ) } C_ ~P A <-> U. { x | ( x C_ A /\ ph /\ ps ) } C_ A )
6	4 5	mpbi	|- U. { x | ( x C_ A /\ ph /\ ps ) } C_ A