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

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )