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	$$⊢\left(A\ne \varnothing \wedge \mathrm{Tr}A\right)\to \varnothing \in A$$

Proof

Step	Hyp	Ref	Expression
1		zfregs	$$⊢A\ne \varnothing \to \exists x\in Ax\cap A=\varnothing$$
2		trss	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\subseteq A\right)$$
3	2	imp	$$⊢\left(\mathrm{Tr}A\wedge x\in A\right)\to x\subseteq A$$
4		dfss	$$⊢x\subseteq A\leftrightarrow x=x\cap A$$
5		eqeq2	$$⊢x\cap A=\varnothing \to \left(x=x\cap A\leftrightarrow x=\varnothing \right)$$
6	4 5	bitrid	$$⊢x\cap A=\varnothing \to \left(x\subseteq A\leftrightarrow x=\varnothing \right)$$
7	3 6	syl5ibcom	$$⊢\left(\mathrm{Tr}A\wedge x\in A\right)\to \left(x\cap A=\varnothing \to x=\varnothing \right)$$
8		eleq1	$$⊢x=\varnothing \to \left(x\in A\leftrightarrow \varnothing \in A\right)$$
9	8	biimpcd	$$⊢x\in A\to \left(x=\varnothing \to \varnothing \in A\right)$$
10	9	adantl	$$⊢\left(\mathrm{Tr}A\wedge x\in A\right)\to \left(x=\varnothing \to \varnothing \in A\right)$$
11	7 10	syld	$$⊢\left(\mathrm{Tr}A\wedge x\in A\right)\to \left(x\cap A=\varnothing \to \varnothing \in A\right)$$
12	11	rexlimdva	$$⊢\mathrm{Tr}A\to \left(\exists x\in Ax\cap A=\varnothing \to \varnothing \in A\right)$$
13	1 12	mpan9	$$⊢\left(A\ne \varnothing \wedge \mathrm{Tr}A\right)\to \varnothing \in A$$