Theorem tr0el

Description: Every nonempty transitive class contains the empty set (/) as an element, a consequence of Regularity and Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		zfregs	|- ( 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	mpan9	|- ( ( A =/= (/) /\ Tr A ) -> (/) e. A )