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

Metamath Proof Explorer

Theorem rexeq

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025)

		Ref	Expression
	Assertion	rexeq	$⊢ 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		anbi1	$⊢ (x \in A \leftrightarrow x \in B) \to ((x \in A \land φ) \leftrightarrow (x \in B \land φ))$
3	2	alexbii	$⊢ \forall x (x \in A \leftrightarrow x \in B) \to (\exists x (x \in A \land φ) \leftrightarrow \exists x (x \in B \land φ))$
4	1 3	sylbi	$⊢ A = B \to (\exists x (x \in A \land φ) \leftrightarrow \exists x (x \in B \land φ))$
5		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
6		df-rex	$⊢ \exists x \in B φ \leftrightarrow \exists x (x \in B \land φ)$
7	4 5 6	3bitr4g	$⊢ A = B \to (\exists x \in A φ \leftrightarrow \exists x \in B φ)$