Metamath Proof Explorer


Theorem cbvabv

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)

Ref Expression
Hypothesis cbvabv.1 x = y φ ψ
Assertion cbvabv x | φ = y | ψ

Proof

Step Hyp Ref Expression
1 cbvabv.1 x = y φ ψ
2 1 cbvsbv z x φ z y ψ
3 df-clab z x | φ z x φ
4 df-clab z y | ψ z y ψ
5 2 3 4 3bitr4i z x | φ z y | ψ
6 5 eqriv x | φ = y | ψ