Theorem gru0eld

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

	Ref	Expression
Hypotheses	gru0eld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
	gru0eld.2	$$⊢\phi \to A\in G$$
Assertion	gru0eld	$$⊢\phi \to \varnothing \in G$$

Proof

Step	Hyp	Ref	Expression
1		gru0eld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
2		gru0eld.2	$$⊢\phi \to A\in G$$
3		0ss	$$⊢\varnothing \subseteq A$$
4	3	a1i	$$⊢\phi \to \varnothing \subseteq A$$
5		gruss	$$⊢\left(G\in \mathrm{Univ}\wedge A\in G\wedge \varnothing \subseteq A\right)\to \varnothing \in G$$
6	1 2 4 5	syl3anc	$$⊢\phi \to \varnothing \in G$$