ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016) (Proof shortened by Wolf Lammen, 22-Jan-2025)

	Ref	Expression
Hypotheses	ceqsex.1	$⊢ Ⅎ x ψ$
	ceqsex.2	$⊢ A \in V$
	ceqsex.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	ceqsex	$⊢ \exists x (x = A \land φ) \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		ceqsex.1	$⊢ Ⅎ x ψ$
2		ceqsex.2	$⊢ A \in V$
3		ceqsex.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
4		alinexa	$⊢ \forall x (x = A \to \neg φ) \leftrightarrow \neg \exists x (x = A \land φ)$
5	1	nfn	$⊢ Ⅎ x \neg ψ$
6	3	notbid	$⊢ x = A \to (\neg φ \leftrightarrow \neg ψ)$
7	5 2 6	ceqsal	$⊢ \forall x (x = A \to \neg φ) \leftrightarrow \neg ψ$
8	4 7	bitr3i	$⊢ \neg \exists x (x = A \land φ) \leftrightarrow \neg ψ$
9	8	con4bii	$⊢ \exists x (x = A \land φ) \leftrightarrow ψ$

Metamath Proof Explorer

Theorem ceqsex

Proof