Metamath Proof Explorer


Theorem mosssn2

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Assertion mosssn2 *xxAyAy

Proof

Step Hyp Ref Expression
1 19.45v yA=A=yA=yA=y
2 sssn AyA=A=y
3 2 exbii yAyyA=A=y
4 mo0sn *xxAA=yA=y
5 1 3 4 3bitr4ri *xxAyAy