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	|- ( A e. V -> ( { (/) } |`t A ) = { (/) } )

Proof

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