Theorem 0thinc

Description: The empty category (see 0cat ) is thin. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Assertion	0thinc	⊢ ∅ ∈ ThinCat

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		base0	⊢ ∅ = ( Base ‘ ∅ )
3		0thincg	⊢ ( ( ∅ ∈ V ∧ ∅ = ( Base ‘ ∅ ) ) → ∅ ∈ ThinCat )
4	1 2 3	mp2an	⊢ ∅ ∈ ThinCat