Metamath Proof Explorer


Theorem eliminable-abeqv

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

Ref Expression
Assertion eliminable-abeqv x|φ=yzzxφzy

Proof

Step Hyp Ref Expression
1 dfcleq x|φ=yzzx|φzy
2 eliminable-velab zx|φzxφ
3 2 bibi1i zx|φzyzxφzy
4 3 albii zzx|φzyzzxφzy
5 1 4 bitri x|φ=yzzxφzy