dfon2lem2

		Ref	Expression
	Assertion	dfon2lem2	$⊢ ⋃ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq A$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (x \subseteq A \land φ \land ψ) \to x \subseteq A$
2	1	ss2abi	$⊢ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq \{x \| x \subseteq A\}$
3		df-pw	$⊢ 𝒫 A = \{x \| x \subseteq A\}$
4	2 3	sseqtrri	$⊢ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq 𝒫 A$
5		sspwuni	$⊢ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq 𝒫 A \leftrightarrow ⋃ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq A$
6	4 5	mpbi	$⊢ ⋃ \{x \| (x \subseteq A \land φ \land ψ)\} \subseteq A$

Metamath Proof Explorer