Metamath Proof Explorer


Theorem cbvalv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require ax-13 . See cbvalvw for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-1993) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses cbvalv1.nf1 y φ
cbvalv1.nf2 x ψ
cbvalv1.1 x = y φ ψ
Assertion cbvalv1 x φ y ψ

Proof

Step Hyp Ref Expression
1 cbvalv1.nf1 y φ
2 cbvalv1.nf2 x ψ
3 cbvalv1.1 x = y φ ψ
4 3 biimpd x = y φ ψ
5 1 2 4 cbv3v x φ y ψ
6 3 biimprd x = y ψ φ
7 6 equcoms y = x ψ φ
8 2 1 7 cbv3v y ψ x φ
9 5 8 impbii x φ y ψ