Metamath Proof Explorer


Theorem snssb

Description: Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025)

Ref Expression
Assertion snssb A B A V A B

Proof

Step Hyp Ref Expression
1 dfss2 A B x x A x B
2 velsn x A x = A
3 2 imbi1i x A x B x = A x B
4 3 albii x x A x B x x = A x B
5 eleq1 x = A x B A B
6 5 pm5.74i x = A x B x = A A B
7 6 albii x x = A x B x x = A A B
8 19.23v x x = A A B x x = A A B
9 isset A V x x = A
10 9 bicomi x x = A A V
11 10 imbi1i x x = A A B A V A B
12 7 8 11 3bitri x x = A x B A V A B
13 1 4 12 3bitri A B A V A B