Theorem bj-restn0b

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

	Ref	Expression
Assertion	bj-restn0b	|- ( ( X e. ( V \ { (/) } ) /\ A e. W ) -> ( X |`t A ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		eldifi	|- ( X e. ( V \ { (/) } ) -> X e. V )
2		eldifsni	|- ( X e. ( V \ { (/) } ) -> X =/= (/) )
3	1 2	jca	|- ( X e. ( V \ { (/) } ) -> ( X e. V /\ X =/= (/) ) )
4	3	anim1i	|- ( ( X e. ( V \ { (/) } ) /\ A e. W ) -> ( ( X e. V /\ X =/= (/) ) /\ A e. W ) )
5		an32	|- ( ( ( X e. V /\ X =/= (/) ) /\ A e. W ) <-> ( ( X e. V /\ A e. W ) /\ X =/= (/) ) )
6	4 5	sylib	|- ( ( X e. ( V \ { (/) } ) /\ A e. W ) -> ( ( X e. V /\ A e. W ) /\ X =/= (/) ) )
7		bj-restn0	|- ( ( X e. V /\ A e. W ) -> ( X =/= (/) -> ( X |`t A ) =/= (/) ) )
8	7	imp	|- ( ( ( X e. V /\ A e. W ) /\ X =/= (/) ) -> ( X |`t A ) =/= (/) )
9	6 8	syl	|- ( ( X e. ( V \ { (/) } ) /\ A e. W ) -> ( X |`t A ) =/= (/) )