Metamath Proof Explorer

Theorem 0elros

Description: A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020)

		Ref	Expression
	Hypothesis	isros.1	\|- Q = { s e. ~P ~P O \| ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
	Assertion	0elros	\|- ( S e. Q -> (/) e. S )

Step	Hyp	Ref	Expression
1		isros.1	\|- Q = { s e. ~P ~P O \| ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
2	1	isros	\|- ( S e. Q <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )
3	2	simp2bi	\|- ( S e. Q -> (/) e. S )

Step

Hyp

Ref

Expression

isros.1

 |-  Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }

 |-  ( S e. Q <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )

 |-  ( S e. Q -> (/) e. S )