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

Metamath Proof Explorer

Theorem cbvex2vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 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
	Hypothesis	cbval2vw.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
	Assertion	cbvex2vw	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$

Proof

Step	Hyp	Ref	Expression
1		cbval2vw.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
2	1	cbvexdvaw	$⊢ x = z \to (\exists y φ \leftrightarrow \exists w ψ)$
3	2	cbvexvw	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$