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 e. V -> ( ( TC ` A ) = (/) <-> A = (/) ) )

Proof

Step Hyp Ref Expression
1 tcid 
 |-  ( A e. V -> A C_ ( TC ` A ) )
2 sseq0 
 |-  ( ( A C_ ( TC ` A ) /\ ( TC ` A ) = (/) ) -> A = (/) )
3 2 ex 
 |-  ( A C_ ( TC ` A ) -> ( ( TC ` A ) = (/) -> A = (/) ) )
4 1 3 syl 
 |-  ( A e. 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 e. V -> ( ( TC ` A ) = (/) <-> A = (/) ) )