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