reueq1OLD

Description: Obsolete version of reueq1 as of 12-Mar-2025. (Contributed by NM, 5-Apr-2004) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ A = B \to (x \in A \leftrightarrow x \in B)$
2	1	anbi1d	$⊢ A = B \to ((x \in A \land φ) \leftrightarrow (x \in B \land φ))$
3	2	eubidv	$⊢ A = B \to (\exists! x (x \in A \land φ) \leftrightarrow \exists! x (x \in B \land φ))$
4		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
5		df-reu	$⊢ \exists! x \in B φ \leftrightarrow \exists! x (x \in B \land φ)$
6	3 4 5	3bitr4g	$⊢ A = B \to (\exists! x \in A φ \leftrightarrow \exists! x \in B φ)$

Metamath Proof Explorer

Theorem reueq1OLD

Proof