Metamath Proof Explorer

Theorem bj-snfromadj

Description: Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

Ref Expression
Assertion bj-snfromadj 
|- { x } e. _V

Proof

Step Hyp Ref Expression
1 0un 
 |-  ( (/) u. { x } ) = { x }
2 0ex 
 |-  (/) e. _V
3 bj-adjg1 
 |-  ( (/) e. _V -> ( (/) u. { x } ) e. _V )
4 2 3 ax-mp 
 |-  ( (/) u. { x } ) e. _V
5 1 4 eqeltrri 
 |-  { x } e. _V