Theorem bj-rest10b

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

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

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( X e. ( V \ { (/) } ) <-> ( X e. V /\ -. X e. { (/) } ) )
2		0ex	|- (/) e. _V
3	2	elsn2	|- ( X e. { (/) } <-> X = (/) )
4		neqne	|- ( -. X = (/) -> X =/= (/) )
5	3 4	sylnbi	|- ( -. X e. { (/) } -> X =/= (/) )
6	5	anim2i	|- ( ( X e. V /\ -. X e. { (/) } ) -> ( X e. V /\ X =/= (/) ) )
7	1 6	sylbi	|- ( X e. ( V \ { (/) } ) -> ( X e. V /\ X =/= (/) ) )
8		bj-rest10	|- ( X e. V -> ( X =/= (/) -> ( X |`t (/) ) = { (/) } ) )
9	8	imp	|- ( ( X e. V /\ X =/= (/) ) -> ( X |`t (/) ) = { (/) } )
10	7 9	syl	|- ( X e. ( V \ { (/) } ) -> ( X |`t (/) ) = { (/) } )