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

Metamath Proof Explorer

Theorem cbvalw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017)

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