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

Metamath Proof Explorer

Theorem rexsn

Description: Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011)

	Ref	Expression
Hypotheses	ralsn.1	$⊢ A \in V$
	ralsn.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	rexsn	$⊢ \exists x \in \{A\} φ \leftrightarrow ψ$

Step	Hyp	Ref	Expression
1		ralsn.1	$⊢ A \in V$
2		ralsn.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3	2	rexsng	$⊢ A \in V \to (\exists x \in \{A\} φ \leftrightarrow ψ)$
4	1 3	ax-mp	$⊢ \exists x \in \{A\} φ \leftrightarrow ψ$