Theorem tr0elw

Description: Every nonempty transitive set contains the empty set (/) as an element, a consequence of Regularity. If we assume Transitive Containment, then we can omit the A e. V hypothesis, see tr0el . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	tr0elw	|- ( ( A e. V /\ A =/= (/) /\ Tr A ) -> (/) e. A )

Proof

Step	Hyp	Ref	Expression
1		zfreg	|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )
2		trss	|- ( Tr A -> ( x e. A -> x C_ A ) )
3	2	imp	|- ( ( Tr A /\ x e. A ) -> x C_ A )
4		dfss	|- ( x C_ A <-> x = ( x i^i A ) )
5		eqeq2	|- ( ( x i^i A ) = (/) -> ( x = ( x i^i A ) <-> x = (/) ) )
6	4 5	bitrid	|- ( ( x i^i A ) = (/) -> ( x C_ A <-> x = (/) ) )
7	3 6	syl5ibcom	|- ( ( Tr A /\ x e. A ) -> ( ( x i^i A ) = (/) -> x = (/) ) )
8		eleq1	|- ( x = (/) -> ( x e. A <-> (/) e. A ) )
9	8	biimpcd	|- ( x e. A -> ( x = (/) -> (/) e. A ) )
10	9	adantl	|- ( ( Tr A /\ x e. A ) -> ( x = (/) -> (/) e. A ) )
11	7 10	syld	|- ( ( Tr A /\ x e. A ) -> ( ( x i^i A ) = (/) -> (/) e. A ) )
12	11	rexlimdva	|- ( Tr A -> ( E. x e. A ( x i^i A ) = (/) -> (/) e. A ) )
13	1 12	syl5com	|- ( ( A e. V /\ A =/= (/) ) -> ( Tr A -> (/) e. A ) )
14	13	3impia	|- ( ( A e. V /\ A =/= (/) /\ Tr A ) -> (/) e. A )