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	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvex2vw	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbval2vw.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
2	1	cbvexdvaw	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 𝜑 ↔ ∃ 𝑤 𝜓 ) )
3	2	cbvexvw	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 )