Metamath Proof Explorer
Description: Change bound variable. Uses only Tarski's FOL axiom schemes.
(Contributed by NM, 9Apr2017)


Ref 
Expression 

Hypotheses 
cbvalw.1 
⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) 


cbvalw.2 
⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 ) 


cbvalw.3 
⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 ∀ 𝑦 𝜓 ) 


cbvalw.4 
⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 ) 


cbvalw.5 
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) 

Assertion 
cbvalw 
⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

cbvalw.1 
⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) 
2 

cbvalw.2 
⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 ) 
3 

cbvalw.3 
⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 ∀ 𝑦 𝜓 ) 
4 

cbvalw.4 
⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 ) 
5 

cbvalw.5 
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) 
6 
5

biimpd 
⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) 
7 
1 2 6

cbvaliw 
⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) 
8 
5

biimprd 
⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) ) 
9 
8

equcoms 
⊢ ( 𝑦 = 𝑥 → ( 𝜓 → 𝜑 ) ) 
10 
3 4 9

cbvaliw 
⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 ) 
11 
7 10

impbii 
⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) 