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\in V\to \left(\mathrm{TC}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		tcid	$$⊢A\in V\to A\subseteq \mathrm{TC}\left(A\right)$$
2		sseq0	$$⊢\left(A\subseteq \mathrm{TC}\left(A\right)\wedge \mathrm{TC}\left(A\right)=\varnothing \right)\to A=\varnothing$$
3	2	ex	$$⊢A\subseteq \mathrm{TC}\left(A\right)\to \left(\mathrm{TC}\left(A\right)=\varnothing \to A=\varnothing \right)$$
4	1 3	syl	$$⊢A\in V\to \left(\mathrm{TC}\left(A\right)=\varnothing \to A=\varnothing \right)$$
5		fveq2	$$⊢A=\varnothing \to \mathrm{TC}\left(A\right)=\mathrm{TC}\left(\varnothing \right)$$
6		tc0	$$⊢\mathrm{TC}\left(\varnothing \right)=\varnothing$$
7	5 6	eqtrdi	$$⊢A=\varnothing \to \mathrm{TC}\left(A\right)=\varnothing$$
8	4 7	impbid1	$$⊢A\in V\to \left(\mathrm{TC}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$