Metamath Proof Explorer

Theorem rexxfrd2

Description: Transfer existence from a variable x to another variable y contained in expression A . Variant of rexxfrd . (Contributed by Alexander van der Vekens, 25-Apr-2018)

		Ref	Expression
	Hypotheses	ralxfrd2.1	$⊢ (φ \land y \in C) \to A \in B$
		ralxfrd2.2	$⊢ (φ \land x \in B) \to \exists y \in C x = A$
		ralxfrd2.3	$⊢ (φ \land y \in C \land x = A) \to (ψ \leftrightarrow χ)$
	Assertion	rexxfrd2	$⊢ φ \to (\exists x \in B ψ \leftrightarrow \exists y \in C χ)$

Proof

Step	Hyp	Ref	Expression
1		ralxfrd2.1	$⊢ (φ \land y \in C) \to A \in B$
2		ralxfrd2.2	$⊢ (φ \land x \in B) \to \exists y \in C x = A$
3		ralxfrd2.3	$⊢ (φ \land y \in C \land x = A) \to (ψ \leftrightarrow χ)$
4	3	notbid	$⊢ (φ \land y \in C \land x = A) \to (\neg ψ \leftrightarrow \neg χ)$
5	1 2 4	ralxfrd2	$⊢ φ \to (\forall x \in B \neg ψ \leftrightarrow \forall y \in C \neg χ)$
6	5	notbid	$⊢ φ \to (\neg \forall x \in B \neg ψ \leftrightarrow \neg \forall y \in C \neg χ)$
7		dfrex2	$⊢ \exists x \in B ψ \leftrightarrow \neg \forall x \in B \neg ψ$
8		dfrex2	$⊢ \exists y \in C χ \leftrightarrow \neg \forall y \in C \neg χ$
9	6 7 8	3bitr4g	$⊢ φ \to (\exists x \in B ψ \leftrightarrow \exists y \in C χ)$