Metamath Proof Explorer

Theorem ralxfrd2

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . Variant of ralxfrd . (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	ralxfrd2	$⊢ φ \to (\forall x \in B ψ \leftrightarrow \forall 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	3expa	$⊢ ((φ \land y \in C) \land x = A) \to (ψ \leftrightarrow χ)$
5	1 4	rspcdv	$⊢ (φ \land y \in C) \to (\forall x \in B ψ \to χ)$
6	5	ralrimdva	$⊢ φ \to (\forall x \in B ψ \to \forall y \in C χ)$
7		r19.29	$⊢ (\forall y \in C χ \land \exists y \in C x = A) \to \exists y \in C (χ \land x = A)$
8	3	ad4ant134	$⊢ (((φ \land x \in B) \land y \in C) \land x = A) \to (ψ \leftrightarrow χ)$
9	8	exbiri	$⊢ ((φ \land x \in B) \land y \in C) \to (x = A \to (χ \to ψ))$
10	9	impcomd	$⊢ ((φ \land x \in B) \land y \in C) \to ((χ \land x = A) \to ψ)$
11	10	rexlimdva	$⊢ (φ \land x \in B) \to (\exists y \in C (χ \land x = A) \to ψ)$
12	7 11	syl5	$⊢ (φ \land x \in B) \to ((\forall y \in C χ \land \exists y \in C x = A) \to ψ)$
13	2 12	mpan2d	$⊢ (φ \land x \in B) \to (\forall y \in C χ \to ψ)$
14	13	ralrimdva	$⊢ φ \to (\forall y \in C χ \to \forall x \in B ψ)$
15	6 14	impbid	$⊢ φ \to (\forall x \in B ψ \leftrightarrow \forall y \in C χ)$