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

Proof

Step	Hyp	Ref	Expression
1		zfreg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )
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	syl5com	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( Tr 𝐴 → ∅ ∈ 𝐴 ) )
14	13	3impia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴 ) → ∅ ∈ 𝐴 )