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

Metamath Proof Explorer

Theorem cbvex4vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex4v with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

		Ref	Expression
	Hypotheses	cbvex4vw.1	$⊢ (x = v \land y = u) \to (φ \leftrightarrow ψ)$
		cbvex4vw.2	$⊢ (z = f \land w = g) \to (ψ \leftrightarrow χ)$
	Assertion	cbvex4vw	$⊢ \exists x \exists y \exists z \exists w φ \leftrightarrow \exists v \exists u \exists f \exists g χ$

Proof

Step	Hyp	Ref	Expression
1		cbvex4vw.1	$⊢ (x = v \land y = u) \to (φ \leftrightarrow ψ)$
2		cbvex4vw.2	$⊢ (z = f \land w = g) \to (ψ \leftrightarrow χ)$
3	1	2exbidv	$⊢ (x = v \land y = u) \to (\exists z \exists w φ \leftrightarrow \exists z \exists w ψ)$
4	3	cbvex2vw	$⊢ \exists x \exists y \exists z \exists w φ \leftrightarrow \exists v \exists u \exists z \exists w ψ$
5	2	cbvex2vw	$⊢ \exists z \exists w ψ \leftrightarrow \exists f \exists g χ$
6	5	2exbii	$⊢ \exists v \exists u \exists z \exists w ψ \leftrightarrow \exists v \exists u \exists f \exists g χ$
7	4 6	bitri	$⊢ \exists x \exists y \exists z \exists w φ \leftrightarrow \exists v \exists u \exists f \exists g χ$