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

Metamath Proof Explorer

Theorem reusng

Description: Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023)

		Ref	Expression
	Hypothesis	ralsng.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	reusng	$⊢ A \in V \to (\exists! x \in \{A\} φ \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		ralsng.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		nfv	$⊢ Ⅎ x ψ$
3	2 1	reusngf	$⊢ A \in V \to (\exists! x \in \{A\} φ \leftrightarrow ψ)$