Theorem gru0eld

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

	Ref	Expression
Hypotheses	gru0eld.1	|- ( ph -> G e. Univ )
	gru0eld.2	|- ( ph -> A e. G )
Assertion	gru0eld	|- ( ph -> (/) e. G )

Proof

Step	Hyp	Ref	Expression
1		gru0eld.1	|- ( ph -> G e. Univ )
2		gru0eld.2	|- ( ph -> A e. G )
3		0ss	|- (/) C_ A
4	3	a1i	|- ( ph -> (/) C_ A )
5		gruss	|- ( ( G e. Univ /\ A e. G /\ (/) C_ A ) -> (/) e. G )
6	1 2 4 5	syl3anc	|- ( ph -> (/) e. G )