Theorem rexab

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014) (Revised by Mario Carneiro, 3-Sep-2015) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024)

	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		dfrex2	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \neg \forall x\in \left\{y|\phi \right\}\neg \chi$$
3	1	ralab	$$⊢\forall x\in \left\{y|\phi \right\}\neg \chi \leftrightarrow \forall x\left(\psi \to \neg \chi \right)$$
4	2 3	xchbinx	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \neg \forall x\left(\psi \to \neg \chi \right)$$
5		imnang	$$⊢\forall x\left(\psi \to \neg \chi \right)\leftrightarrow \forall x\neg \left(\psi \wedge \chi \right)$$
6	4 5	xchbinx	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \neg \forall x\neg \left(\psi \wedge \chi \right)$$
7		df-ex	$$⊢\exists x\left(\psi \wedge \chi \right)\leftrightarrow \neg \forall x\neg \left(\psi \wedge \chi \right)$$
8	6 7	bitr4i	$$⊢\exists x\in \left\{y|\phi \right\}\chi \leftrightarrow \exists x\left(\psi \wedge \chi \right)$$