Metamath Proof Explorer


Theorem elrabiOLD

Description: Obsolete version of elrabi as of 5-Aug-2024. (Contributed by Alexander van der Vekens, 31-Dec-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion elrabiOLD A x V | φ A V

Proof

Step Hyp Ref Expression
1 clelab A x | x V φ x x = A x V φ
2 eleq1 x = A x V A V
3 2 anbi1d x = A x V φ A V φ
4 3 simprbda x = A x V φ A V
5 4 exlimiv x x = A x V φ A V
6 1 5 sylbi A x | x V φ A V
7 df-rab x V | φ = x | x V φ
8 6 7 eleq2s A x V | φ A V