Description: Weaker version of eleq2 (but more general than elequ2 ) not depending on ax-ext nor df-cleq . (Contributed by BJ, 29-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | eleq2w | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 | |
|
2 | 1 | anbi2d | |
3 | 2 | exbidv | |
4 | dfclel | |
|
5 | dfclel | |
|
6 | 3 4 5 | 3bitr4g | |