Metamath Proof Explorer


Theorem eliminable-veqab

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

Ref Expression
Assertion eliminable-veqab 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 y | φ z y φ
3 2 bibi2i z x z y | φ z x z y φ
4 3 albii z z x z y | φ z z x z y φ
5 1 4 bitri x = y | φ z z x z y φ