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

Metamath Proof Explorer

Theorem rexeqbidv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007) Remove usage of ax-10 , ax-11 , and ax-12 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023)

	Ref	Expression
Hypotheses	raleqbidv.1	$⊢ φ \to A = B$
	raleqbidv.2	$⊢ φ \to (ψ \leftrightarrow χ)$
Assertion	rexeqbidv	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B χ)$

Proof

Step	Hyp	Ref	Expression
1		raleqbidv.1	$⊢ φ \to A = B$
2		raleqbidv.2	$⊢ φ \to (ψ \leftrightarrow χ)$
3	1	eleq2d	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
4	3 2	anbi12d	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land χ))$
5	4	rexbidv2	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B χ)$