Metamath Proof Explorer


Theorem eliminable-abelv

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

Ref Expression
Assertion eliminable-abelv x | φ y z t t z t x φ z y

Proof

Step Hyp Ref Expression
1 dfclel x | φ y z z = x | φ z y
2 eliminable-veqab z = x | φ t t z t x φ
3 2 anbi1i z = x | φ z y t t z t x φ z y
4 3 exbii z z = x | φ z y z t t z t x φ z y
5 1 4 bitri x | φ y z t t z t x φ z y