Theorem cbval2vw

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

	Ref	Expression
Hypothesis	cbval2vw.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbval2vw	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbval2vw.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
2	1	cbvaldvaw	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 𝜑 ↔ ∀ 𝑤 𝜓 ) )
3	2	cbvalvw	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )