Theorem dfon2lem2

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

	Ref	Expression
Assertion	dfon2lem2	$$⊢\bigcup \left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(x\subseteq A\wedge \phi \wedge \psi \right)\to x\subseteq A$$
2	1	ss2abi	$$⊢\left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq \left\{x|x\subseteq A\right\}$$
3		df-pw	$$⊢𝒫A=\left\{x|x\subseteq A\right\}$$
4	2 3	sseqtrri	$$⊢\left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq 𝒫A$$
5		sspwuni	$$⊢\left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq 𝒫A\leftrightarrow \bigcup \left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq A$$
6	4 5	mpbi	$$⊢\bigcup \left\{x|\left(x\subseteq A\wedge \phi \wedge \psi \right)\right\}\subseteq A$$