Metamath Proof Explorer

Theorem bj-restsn10

Description: Special case of bj-restsn , bj-restsnss , and bj-rest10 . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restsn10 
|- ( X e. V -> ( { X } |`t (/) ) = { (/) } )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ X
2 bj-restsnss 
 |-  ( ( X e. V /\ (/) C_ X ) -> ( { X } |`t (/) ) = { (/) } )
3 1 2 mpan2 
 |-  ( X e. V -> ( { X } |`t (/) ) = { (/) } )