Theorem bj-rest10b

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

	Ref	Expression
Assertion	bj-rest10b	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝑋 ↾t ∅ ) = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) ↔ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ { ∅ } ) )
2		0ex	⊢ ∅ ∈ V
3	2	elsn2	⊢ ( 𝑋 ∈ { ∅ } ↔ 𝑋 = ∅ )
4		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
5	3 4	sylnbi	⊢ ( ¬ 𝑋 ∈ { ∅ } → 𝑋 ≠ ∅ )
6	5	anim2i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ { ∅ } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) )
7	1 6	sylbi	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) )
8		bj-rest10	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t ∅ ) = { ∅ } ) )
9	8	imp	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ↾t ∅ ) = { ∅ } )
10	7 9	syl	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝑋 ↾t ∅ ) = { ∅ } )