Metamath Proof Explorer


Theorem moel

Description: "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018) Avoid ax-11 . (Revised by Wolf Lammen, 23-Nov-2024)

Ref Expression
Assertion moel * x x A x A y A x = y

Proof

Step Hyp Ref Expression
1 19.21v y x A y A x = y x A y y A x = y
2 impexp x A y A x = y x A y A x = y
3 2 albii y x A y A x = y y x A y A x = y
4 df-ral y A x = y y y A x = y
5 4 imbi2i x A y A x = y x A y y A x = y
6 1 3 5 3bitr4i y x A y A x = y x A y A x = y
7 6 albii x y x A y A x = y x x A y A x = y
8 eleq1w x = y x A y A
9 8 mo4 * x x A x y x A y A x = y
10 df-ral x A y A x = y x x A y A x = y
11 7 9 10 3bitr4i * x x A x A y A x = y