bj-restn0b

Description: Alternate version of bj-restn0 . (Contributed by BJ, 27-Apr-2021)

		Ref	Expression
	Assertion	bj-restn0b	$⊢ (X \in (V ∖ \{\emptyset\}) \land A \in W) \to X ↾_{𝑡} A \neq \emptyset$

Step	Hyp	Ref	Expression
1		eldifi	$⊢ X \in (V ∖ \{\emptyset\}) \to X \in V$
2		eldifsni	$⊢ X \in (V ∖ \{\emptyset\}) \to X \neq \emptyset$
3	1 2	jca	$⊢ X \in (V ∖ \{\emptyset\}) \to (X \in V \land X \neq \emptyset)$
4	3	anim1i	$⊢ (X \in (V ∖ \{\emptyset\}) \land A \in W) \to ((X \in V \land X \neq \emptyset) \land A \in W)$
5		an32	$⊢ ((X \in V \land X \neq \emptyset) \land A \in W) \leftrightarrow ((X \in V \land A \in W) \land X \neq \emptyset)$
6	4 5	sylib	$⊢ (X \in (V ∖ \{\emptyset\}) \land A \in W) \to ((X \in V \land A \in W) \land X \neq \emptyset)$
7		bj-restn0	$⊢ (X \in V \land A \in W) \to (X \neq \emptyset \to X ↾_{𝑡} A \neq \emptyset)$
8	7	imp	$⊢ ((X \in V \land A \in W) \land X \neq \emptyset) \to X ↾_{𝑡} A \neq \emptyset$
9	6 8	syl	$⊢ (X \in (V ∖ \{\emptyset\}) \land A \in W) \to X ↾_{𝑡} A \neq \emptyset$

Metamath Proof Explorer