Theorem bj-restsn0

Description: An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn and bj-restsnss2 . TODO: this is restsn . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsn0	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } ↾t 𝐴 ) = { ∅ } )

Proof

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