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

Metamath Proof Explorer

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 GG, 2-Nov-2024)

		Ref	Expression
	Hypothesis	ralab.1	$⊢ y = x \to (φ \leftrightarrow ψ)$
	Assertion	rexab	$⊢ \exists x \in \{y \| φ\} χ \leftrightarrow \exists x (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		ralab.1	$⊢ y = x \to (φ \leftrightarrow ψ)$
2		dfrex2	$⊢ \exists x \in \{y \| φ\} χ \leftrightarrow \neg \forall x \in \{y \| φ\} \neg χ$
3	1	ralab	$⊢ \forall x \in \{y \| φ\} \neg χ \leftrightarrow \forall x (ψ \to \neg χ)$
4	2 3	xchbinx	$⊢ \exists x \in \{y \| φ\} χ \leftrightarrow \neg \forall x (ψ \to \neg χ)$
5		imnang	$⊢ \forall x (ψ \to \neg χ) \leftrightarrow \forall x \neg (ψ \land χ)$
6	4 5	xchbinx	$⊢ \exists x \in \{y \| φ\} χ \leftrightarrow \neg \forall x \neg (ψ \land χ)$
7		df-ex	$⊢ \exists x (ψ \land χ) \leftrightarrow \neg \forall x \neg (ψ \land χ)$
8	6 7	bitr4i	$⊢ \exists x \in \{y \| φ\} χ \leftrightarrow \exists x (ψ \land χ)$