Theorem rexab

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexab	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \exists x\left(\psi \wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralab.1	$$⊢y=x\to \left(\phi \leftrightarrow \psi \right)$$
2		df-rex	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \exists x\left(x\in \left\{y|\phi \right\}\wedge \chi \right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3 1	elab	$$⊢x\in \left\{y|\phi \right\}\leftrightarrow \psi$$
5	4	anbi1i	$$⊢\left(x\in \left\{y|\phi \right\}\wedge \chi \right)\leftrightarrow \left(\psi \wedge \chi \right)$$
6	5	exbii	$$⊢\exists x\left(x\in \left\{y|\phi \right\}\wedge \chi \right)\leftrightarrow \exists x\left(\psi \wedge \chi \right)$$
7	2 6	bitri	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \exists x\left(\psi \wedge \chi \right)$$