Metamath Proof Explorer


Theorem eliminable-abelab

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

Ref Expression
Assertion eliminable-abelab 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 eliminable-velab z y | ψ z y ψ
4 2 3 anbi12i z = x | φ z y | ψ t t z t x φ z y ψ
5 4 exbii z z = x | φ z y | ψ z t t z t x φ z y ψ
6 1 5 bitri x | φ y | ψ z t t z t x φ z y ψ