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)