Theorem bj-restn0b

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

	Ref	Expression
Assertion	bj-restn0b	⊢ ( ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ↾t 𝐴 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → 𝑋 ∈ 𝑉 )
2		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → 𝑋 ≠ ∅ )
3	1 2	jca	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) )
4	3	anim1i	⊢ ( ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) ∧ 𝐴 ∈ 𝑊 ) )
5		an32	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) ∧ 𝐴 ∈ 𝑊 ) ↔ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ 𝑋 ≠ ∅ ) )
6	4 5	sylib	⊢ ( ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ 𝑋 ≠ ∅ ) )
7		bj-restn0	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t 𝐴 ) ≠ ∅ ) )
8	7	imp	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ↾t 𝐴 ) ≠ ∅ )
9	6 8	syl	⊢ ( ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ↾t 𝐴 ) ≠ ∅ )