Metamath Proof Explorer


Theorem moel

Description: "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 ralcom4 x A y y A x = y y x A y A x = y
2 df-ral y A x = y y y A x = y
3 2 ralbii x A y A x = y x A y y A x = y
4 alcom x y x A y A x = y y x x A y A x = y
5 eleq1w x = y x A y A
6 5 mo4 * x x A x y x A y A x = y
7 df-ral x A y A x = y x x A y A x = y
8 impexp x A y A x = y x A y A x = y
9 8 albii x x A y A x = y x x A y A x = y
10 7 9 bitr4i x A y A x = y x x A y A x = y
11 10 albii y x A y A x = y y x x A y A x = y
12 4 6 11 3bitr4i * x x A y x A y A x = y
13 1 3 12 3bitr4ri * x x A x A y A x = y