Metamath Proof Explorer


Theorem bj-rest0

Description: An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-rest0 X V A W X X 𝑡 A

Proof

Step Hyp Ref Expression
1 in0 A =
2 incom A = A
3 1 2 eqtr3i = A
4 0ex V
5 eleq1 x = x X X
6 ineq1 x = x A = A
7 6 eqeq2d x = = x A = A
8 5 7 anbi12d x = x X = x A X = A
9 4 8 spcev X = A x x X = x A
10 3 9 mpan2 X x x X = x A
11 df-rex x X = x A x x X = x A
12 10 11 sylibr X x X = x A
13 elrest X V A W X 𝑡 A x X = x A
14 12 13 syl5ibr X V A W X X 𝑡 A