Metamath Proof Explorer


Theorem cbvalvw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 28-Feb-2018)

Ref Expression
Hypothesis cbvalvw.1 x = y φ ψ
Assertion cbvalvw x φ y ψ

Proof

Step Hyp Ref Expression
1 cbvalvw.1 x = y φ ψ
2 ax-5 x φ y x φ
3 ax-5 ¬ ψ x ¬ ψ
4 ax-5 y ψ x y ψ
5 ax-5 ¬ φ y ¬ φ
6 2 3 4 5 1 cbvalw x φ y ψ