Metamath Proof Explorer


Theorem cbvabwOLD

Description: Obsolete version of cbvabw as of 23-May-2024. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbvabw.1 y φ
cbvabw.2 x ψ
cbvabw.3 x = y φ ψ
Assertion cbvabwOLD x | φ = y | ψ

Proof

Step Hyp Ref Expression
1 cbvabw.1 y φ
2 cbvabw.2 x ψ
3 cbvabw.3 x = y φ ψ
4 1 sbco2v z y y x φ z x φ
5 2 3 sbiev y x φ ψ
6 5 sbbii z y y x φ z y ψ
7 4 6 bitr3i z x φ z y ψ
8 df-clab z x | φ z x φ
9 df-clab z y | ψ z y ψ
10 7 8 9 3bitr4i z x | φ z y | ψ
11 10 eqriv x | φ = y | ψ