This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tc00

Description: The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

Ref Expression
Assertion tc00 ⊢ A ∈ V → TC ⁡ A = ∅ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 tcid ⊢ A ∈ V → A ⊆ TC ⁡ A
2 sseq0 ⊢ A ⊆ TC ⁡ A ∧ TC ⁡ A = ∅ → A = ∅
3 2 ex ⊢ A ⊆ TC ⁡ A → TC ⁡ A = ∅ → A = ∅
4 1 3 syl ⊢ A ∈ V → TC ⁡ A = ∅ → A = ∅
5 fveq2 ⊢ A = ∅ → TC ⁡ A = TC ⁡ ∅
6 tc0 ⊢ TC ⁡ ∅ = ∅
7 5 6 eqtrdi ⊢ A = ∅ → TC ⁡ A = ∅
8 4 7 impbid1 ⊢ A ∈ V → TC ⁡ A = ∅ ↔ A = ∅