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 e. V /\ A e. W ) -> ( (/) e. X -> (/) e. ( X |`t A ) ) )

Proof

Step Hyp Ref Expression
1 in0
 |-  ( A i^i (/) ) = (/)
2 incom
 |-  ( A i^i (/) ) = ( (/) i^i A )
3 1 2 eqtr3i
 |-  (/) = ( (/) i^i A )
4 0ex
 |-  (/) e. _V
5 eleq1
 |-  ( x = (/) -> ( x e. X <-> (/) e. X ) )
6 ineq1
 |-  ( x = (/) -> ( x i^i A ) = ( (/) i^i A ) )
7 6 eqeq2d
 |-  ( x = (/) -> ( (/) = ( x i^i A ) <-> (/) = ( (/) i^i A ) ) )
8 5 7 anbi12d
 |-  ( x = (/) -> ( ( x e. X /\ (/) = ( x i^i A ) ) <-> ( (/) e. X /\ (/) = ( (/) i^i A ) ) ) )
9 4 8 spcev
 |-  ( ( (/) e. X /\ (/) = ( (/) i^i A ) ) -> E. x ( x e. X /\ (/) = ( x i^i A ) ) )
10 3 9 mpan2
 |-  ( (/) e. X -> E. x ( x e. X /\ (/) = ( x i^i A ) ) )
11 df-rex
 |-  ( E. x e. X (/) = ( x i^i A ) <-> E. x ( x e. X /\ (/) = ( x i^i A ) ) )
12 10 11 sylibr
 |-  ( (/) e. X -> E. x e. X (/) = ( x i^i A ) )
13 elrest
 |-  ( ( X e. V /\ A e. W ) -> ( (/) e. ( X |`t A ) <-> E. x e. X (/) = ( x i^i A ) ) )
14 12 13 syl5ibr
 |-  ( ( X e. V /\ A e. W ) -> ( (/) e. X -> (/) e. ( X |`t A ) ) )