Metamath Proof Explorer


Theorem eleq2w

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 x=yAxAy

Proof

Step Hyp Ref Expression
1 elequ2 x=yzxzy
2 1 anbi2d x=yz=Azxz=Azy
3 2 exbidv x=yzz=Azxzz=Azy
4 dfclel Axzz=Azx
5 dfclel Ayzz=Azy
6 3 4 5 3bitr4g x=yAxAy