reueq1

Description: Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Avoid ax-8 . (Revised by Wolf Lammen, 12-Mar-2025)

		Ref	Expression
	Assertion	reueq1	$⊢ A = B \to (\exists! x \in A φ \leftrightarrow \exists! x \in B φ)$

Proof

Step	Hyp	Ref	Expression
1		rexeq	$⊢ A = B \to (\exists x \in A φ \leftrightarrow \exists x \in B φ)$
2		rmoeq1	$⊢ A = B \to (\exists^{} x \in A φ \leftrightarrow \exists^{} x \in B φ)$
3	1 2	anbi12d	$⊢ A = B \to ((\exists x \in A φ \land \exists^{} x \in A φ) \leftrightarrow (\exists x \in B φ \land \exists^{} x \in B φ))$
4		reu5	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists^{*} x \in A φ)$
5		reu5	$⊢ \exists! x \in B φ \leftrightarrow (\exists x \in B φ \land \exists^{*} x \in B φ)$
6	3 4 5	3bitr4g	$⊢ A = B \to (\exists! x \in A φ \leftrightarrow \exists! x \in B φ)$

Metamath Proof Explorer

Theorem reueq1

Proof