Theorem tcsni

Description: The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

	Ref	Expression
Hypothesis	tc2.1	|- A e. _V
Assertion	tcsni	|- ( TC ` { A } ) = ( ( TC ` A ) u. { A } )

Proof

Step	Hyp	Ref	Expression
1		tc2.1	|- A e. _V
2	1	snss	|- ( A e. x <-> { A } C_ x )
3	2	anbi1i	|- ( ( A e. x /\ Tr x ) <-> ( { A } C_ x /\ Tr x ) )
4	3	abbii	|- { x | ( A e. x /\ Tr x ) } = { x | ( { A } C_ x /\ Tr x ) }
5	4	inteqi	|- |^| { x | ( A e. x /\ Tr x ) } = |^| { x | ( { A } C_ x /\ Tr x ) }
6	1	tc2	|- ( ( TC ` A ) u. { A } ) = |^| { x | ( A e. x /\ Tr x ) }
7		snex	|- { A } e. _V
8		tcvalg	|- ( { A } e. _V -> ( TC ` { A } ) = |^| { x | ( { A } C_ x /\ Tr x ) } )
9	7 8	ax-mp	|- ( TC ` { A } ) = |^| { x | ( { A } C_ x /\ Tr x ) }
10	5 6 9	3eqtr4ri	|- ( TC ` { A } ) = ( ( TC ` A ) u. { A } )