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	⊢ ( ( 𝐴 ≠ ∅ ∧ Tr 𝐴 ) → ∅ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zfregs	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )
2		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
3	2	imp	⊢ ( ( Tr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝐴 )
4		dfss	⊢ ( 𝑥 ⊆ 𝐴 ↔ 𝑥 = ( 𝑥 ∩ 𝐴 ) )
5		eqeq2	⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ → ( 𝑥 = ( 𝑥 ∩ 𝐴 ) ↔ 𝑥 = ∅ ) )
6	4 5	bitrid	⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 = ∅ ) )
7	3 6	syl5ibcom	⊢ ( ( Tr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∩ 𝐴 ) = ∅ → 𝑥 = ∅ ) )
8		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
9	8	biimpcd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = ∅ → ∅ ∈ 𝐴 ) )
10	9	adantl	⊢ ( ( Tr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = ∅ → ∅ ∈ 𝐴 ) )
11	7 10	syld	⊢ ( ( Tr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∩ 𝐴 ) = ∅ → ∅ ∈ 𝐴 ) )
12	11	rexlimdva	⊢ ( Tr 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ → ∅ ∈ 𝐴 ) )
13	1 12	mpan9	⊢ ( ( 𝐴 ≠ ∅ ∧ Tr 𝐴 ) → ∅ ∈ 𝐴 )