Theorem cbval2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbval2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 22-Dec-2003) (Revised by BJ, 16-Jun-2019) (Proof shortened by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbval2v.1	⊢ Ⅎ 𝑧 𝜑
	cbval2v.2	⊢ Ⅎ 𝑤 𝜑
	cbval2v.3	⊢ Ⅎ 𝑥 𝜓
	cbval2v.4	⊢ Ⅎ 𝑦 𝜓
	cbval2v.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbval2v	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbval2v.1	⊢ Ⅎ 𝑧 𝜑
2		cbval2v.2	⊢ Ⅎ 𝑤 𝜑
3		cbval2v.3	⊢ Ⅎ 𝑥 𝜓
4		cbval2v.4	⊢ Ⅎ 𝑦 𝜓
5		cbval2v.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
6	1	nfal	⊢ Ⅎ 𝑧 ∀ 𝑦 𝜑
7	3	nfal	⊢ Ⅎ 𝑥 ∀ 𝑤 𝜓
8		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝑧
9		nfv	⊢ Ⅎ 𝑤 𝑥 = 𝑧
10	2	a1i	⊢ ( 𝑥 = 𝑧 → Ⅎ 𝑤 𝜑 )
11	4	a1i	⊢ ( 𝑥 = 𝑧 → Ⅎ 𝑦 𝜓 )
12	5	ex	⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 → ( 𝜑 ↔ 𝜓 ) ) )
13	8 9 10 11 12	cbv2w	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 𝜑 ↔ ∀ 𝑤 𝜓 ) )
14	6 7 13	cbvalv1	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )