rexeqf

Description: Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 9-Mar-2025)

	Ref	Expression
Hypotheses	raleqf.1	$⊢ \underline{Ⅎ} x A$
	raleqf.2	$⊢ \underline{Ⅎ} x B$
Assertion	rexeqf	$⊢ A = B \to (\exists x \in A φ \leftrightarrow \exists x \in B φ)$

Proof

Step	Hyp	Ref	Expression
1		raleqf.1	$⊢ \underline{Ⅎ} x A$
2		raleqf.2	$⊢ \underline{Ⅎ} x B$
3	1 2	raleqf	$⊢ A = B \to (\forall x \in A \neg φ \leftrightarrow \forall x \in B \neg φ)$
4		ralnex	$⊢ \forall x \in A \neg φ \leftrightarrow \neg \exists x \in A φ$
5		ralnex	$⊢ \forall x \in B \neg φ \leftrightarrow \neg \exists x \in B φ$
6	3 4 5	3bitr3g	$⊢ A = B \to (\neg \exists x \in A φ \leftrightarrow \neg \exists x \in B φ)$
7	6	con4bid	$⊢ A = B \to (\exists x \in A φ \leftrightarrow \exists x \in B φ)$

Metamath Proof Explorer

Theorem rexeqf

Proof