Theorem gru0eld

Description: A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	gru0eld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	gru0eld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
Assertion	gru0eld	⊢ ( 𝜑 → ∅ ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		gru0eld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		gru0eld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
3		0ss	⊢ ∅ ⊆ 𝐴
4	3	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝐴 )
5		gruss	⊢ ( ( 𝐺 ∈ Univ ∧ 𝐴 ∈ 𝐺 ∧ ∅ ⊆ 𝐴 ) → ∅ ∈ 𝐺 )
6	1 2 4 5	syl3anc	⊢ ( 𝜑 → ∅ ∈ 𝐺 )