Metamath Proof Explorer


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 V 𝑡 A =

Proof

Step Hyp Ref Expression
1 0ss A
2 bj-restsnss2 A V A 𝑡 A =
3 1 2 mpan2 A V 𝑡 A =