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 | ψ


Step Hyp Ref Expression
1 cbvabv.1 x = y φ ψ
2 sbco2vv z y y x φ z x φ
3 1 sbievw y x φ ψ
4 3 sbbii z y y x φ z y ψ
5 2 4 bitr3i z x φ z y ψ
6 df-clab z x | φ z x φ
7 df-clab z y | ψ z y ψ
8 5 6 7 3bitr4i z x | φ z y | ψ
9 8 eqriv x | φ = y | ψ