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

Metamath Proof Explorer

Theorem rexeqbidvvOLD

Description: Obsolete version of rexeqbidvv as of 9-Mar-2025. (Contributed by Wolf Lammen, 25-Sep-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		raleqbidvv.1	$⊢ φ \to A = B$
2		raleqbidvv.2	$⊢ φ \to (ψ \leftrightarrow χ)$
3	2	notbid	$⊢ φ \to (\neg ψ \leftrightarrow \neg χ)$
4	1 3	raleqbidvv	$⊢ φ \to (\forall x \in A \neg ψ \leftrightarrow \forall x \in B \neg χ)$
5		ralnex	$⊢ \forall x \in A \neg ψ \leftrightarrow \neg \exists x \in A ψ$
6		ralnex	$⊢ \forall x \in B \neg χ \leftrightarrow \neg \exists x \in B χ$
7	4 5 6	3bitr3g	$⊢ φ \to (\neg \exists x \in A ψ \leftrightarrow \neg \exists x \in B χ)$
8	7	con4bid	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B χ)$