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	⊢ ( 𝑋 ∈ 𝑉 → ( { 𝑋 } ↾t ∅ ) = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝑋
2		bj-restsnss	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∅ ⊆ 𝑋 ) → ( { 𝑋 } ↾t ∅ ) = { ∅ } )
3	1 2	mpan2	⊢ ( 𝑋 ∈ 𝑉 → ( { 𝑋 } ↾t ∅ ) = { ∅ } )