Metamath Proof Explorer

Theorem eleq1w

Description: Weaker version of eleq1 (but more general than elequ1 ) not depending on ax-ext nor df-cleq .

Note that this provides a proof of ax-8 from Tarski's FOL and dfclel (simply consider an instance where A is replaced by a setvar and deduce the forward implication by biimpd ), which shows that dfclel is too powerful to be used as a definition instead of df-clel . (Contributed by BJ, 24-Jun-2019)

Ref Expression
Assertion eleq1w x = y x A y A


Step Hyp Ref Expression
1 equequ2 x = y z = x z = y
2 1 anbi1d x = y z = x z A z = y z A
3 2 exbidv x = y z z = x z A z z = y z A
4 dfclel x A z z = x z A
5 dfclel y A z z = y z A
6 3 4 5 3bitr4g x = y x A y A