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	$$⊢\left(X\in V\wedge A\in W\right)\to \left(\varnothing \in X\to \varnothing \in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		in0	$$⊢A\cap \varnothing =\varnothing$$
2		incom	$$⊢A\cap \varnothing =\varnothing \cap A$$
3	1 2	eqtr3i	$$⊢\varnothing =\varnothing \cap A$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		eleq1	$$⊢x=\varnothing \to \left(x\in X\leftrightarrow \varnothing \in X\right)$$
6		ineq1	$$⊢x=\varnothing \to x\cap A=\varnothing \cap A$$
7	6	eqeq2d	$$⊢x=\varnothing \to \left(\varnothing =x\cap A\leftrightarrow \varnothing =\varnothing \cap A\right)$$
8	5 7	anbi12d	$$⊢x=\varnothing \to \left(\left(x\in X\wedge \varnothing =x\cap A\right)\leftrightarrow \left(\varnothing \in X\wedge \varnothing =\varnothing \cap A\right)\right)$$
9	4 8	spcev	$$⊢\left(\varnothing \in X\wedge \varnothing =\varnothing \cap A\right)\to \exists x\left(x\in X\wedge \varnothing =x\cap A\right)$$
10	3 9	mpan2	$$⊢\varnothing \in X\to \exists x\left(x\in X\wedge \varnothing =x\cap A\right)$$
11		df-rex	$$⊢\exists x\in X\varnothing =x\cap A\leftrightarrow \exists x\left(x\in X\wedge \varnothing =x\cap A\right)$$
12	10 11	sylibr	$$⊢\varnothing \in X\to \exists x\in X\varnothing =x\cap A$$
13		elrest	$$⊢\left(X\in V\wedge A\in W\right)\to \left(\varnothing \in \left(X{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in X\varnothing =x\cap A\right)$$
14	12 13	imbitrrid	$$⊢\left(X\in V\wedge A\in W\right)\to \left(\varnothing \in X\to \varnothing \in \left(X{\upharpoonright }_{𝑡}A\right)\right)$$