Metamath Proof Explorer


Theorem cbvexvw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 cbvalvw.1 x = y φ ψ
2 1 notbid x = y ¬ φ ¬ ψ
3 2 cbvalvw x ¬ φ y ¬ ψ
4 3 notbii ¬ x ¬ φ ¬ y ¬ ψ
5 df-ex x φ ¬ x ¬ φ
6 df-ex y ψ ¬ y ¬ ψ
7 4 5 6 3bitr4i x φ y ψ