Metamath Proof Explorer

Theorem rmoeq1

Description: Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017) 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	rmoeq1	$⊢ A = B \to (\exists^{} x \in A φ \leftrightarrow \exists^{} x \in B φ)$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$⊢ A = B \leftrightarrow \forall x (x \in A \leftrightarrow x \in B)$
2	1	biimpi	$⊢ A = B \to \forall x (x \in A \leftrightarrow x \in B)$
3		anbi1	$⊢ (x \in A \leftrightarrow x \in B) \to ((x \in A \land φ) \leftrightarrow (x \in B \land φ))$
4	3	imbi1d	$⊢ (x \in A \leftrightarrow x \in B) \to (((x \in A \land φ) \to x = z) \leftrightarrow ((x \in B \land φ) \to x = z))$
5	4	alimi	$⊢ \forall x (x \in A \leftrightarrow x \in B) \to \forall x (((x \in A \land φ) \to x = z) \leftrightarrow ((x \in B \land φ) \to x = z))$
6		albi	$⊢ \forall x (((x \in A \land φ) \to x = z) \leftrightarrow ((x \in B \land φ) \to x = z)) \to (\forall x ((x \in A \land φ) \to x = z) \leftrightarrow \forall x ((x \in B \land φ) \to x = z))$
7	2 5 6	3syl	$⊢ A = B \to (\forall x ((x \in A \land φ) \to x = z) \leftrightarrow \forall x ((x \in B \land φ) \to x = z))$
8	7	exbidv	$⊢ A = B \to (\exists z \forall x ((x \in A \land φ) \to x = z) \leftrightarrow \exists z \forall x ((x \in B \land φ) \to x = z))$
9		df-mo	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \exists z \forall x ((x \in A \land φ) \to x = z)$
10		df-mo	$⊢ \exists^{*} x (x \in B \land φ) \leftrightarrow \exists z \forall x ((x \in B \land φ) \to x = z)$
11	8 9 10	3bitr4g	$⊢ A = B \to (\exists^{} x (x \in A \land φ) \leftrightarrow \exists^{} x (x \in B \land φ))$
12		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
13		df-rmo	$⊢ \exists^{} x \in B φ \leftrightarrow \exists^{} x (x \in B \land φ)$
14	11 12 13	3bitr4g	$⊢ A = B \to (\exists^{} x \in A φ \leftrightarrow \exists^{} x \in B φ)$