abssexg

Description: Existence of a class of subsets. (Contributed by NM, 15-Jul-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011)

		Ref	Expression
	Assertion	abssexg	$⊢ A \in V \to \{x \| (x \subseteq A \land φ)\} \in V$

Step	Hyp	Ref	Expression
1		pwexg	$⊢ A \in V \to 𝒫 A \in V$
2		df-pw	$⊢ 𝒫 A = \{x \| x \subseteq A\}$
3	2	eleq1i	$⊢ 𝒫 A \in V \leftrightarrow \{x \| x \subseteq A\} \in V$
4		simpl	$⊢ (x \subseteq A \land φ) \to x \subseteq A$
5	4	ss2abi	$⊢ \{x \| (x \subseteq A \land φ)\} \subseteq \{x \| x \subseteq A\}$
6		ssexg	$⊢ (\{x \| (x \subseteq A \land φ)\} \subseteq \{x \| x \subseteq A\} \land \{x \| x \subseteq A\} \in V) \to \{x \| (x \subseteq A \land φ)\} \in V$
7	5 6	mpan	$⊢ \{x \| x \subseteq A\} \in V \to \{x \| (x \subseteq A \land φ)\} \in V$
8	3 7	sylbi	$⊢ 𝒫 A \in V \to \{x \| (x \subseteq A \land φ)\} \in V$
9	1 8	syl	$⊢ A \in V \to \{x \| (x \subseteq A \land φ)\} \in V$

Metamath Proof Explorer