Metamath Proof Explorer


Theorem eliminable-abeqab

Description: A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals abstraction. (Contributed by BJ, 30-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion eliminable-abeqab x | φ = y | ψ z z x φ z y ψ

Proof

Step Hyp Ref Expression
1 dfcleq x | φ = y | ψ z z x | φ z y | ψ
2 eliminable-velab z x | φ z x φ
3 eliminable-velab z y | ψ z y ψ
4 2 3 bibi12i z x | φ z y | ψ z x φ z y ψ
5 4 albii z z x | φ z y | ψ z z x φ z y ψ
6 1 5 bitri x | φ = y | ψ z z x φ z y ψ