This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rab2ex

Description: A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	rab2ex.1	$⊢ B = \{y \in A \| ψ\}$
	rab2ex.2	$⊢ A \in V$
Assertion	rab2ex	$⊢ \{x \in B \| φ\} \in V$

Proof

Step	Hyp	Ref	Expression
1		rab2ex.1	$⊢ B = \{y \in A \| ψ\}$
2		rab2ex.2	$⊢ A \in V$
3	1 2	rabex2	$⊢ B \in V$
4	3	rabex	$⊢ \{x \in B \| φ\} \in V$