Theorem nfttc

Description: Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypothesis	nfttc.1	|- F/_ x A
Assertion	nfttc	|- F/_ x TC+ A

Proof

Step	Hyp	Ref	Expression
1		nfttc.1	|- F/_ x A
2		df-ttc	|- TC+ A = U_ y e. A U. ( rec ( ( z e. _V |-> U. z ) , { y } ) " _om )
3		nfcv	|- F/_ x U. ( rec ( ( z e. _V |-> U. z ) , { y } ) " _om )
4	1 3	nfiun	|- F/_ x U_ y e. A U. ( rec ( ( z e. _V |-> U. z ) , { y } ) " _om )
5	2 4	nfcxfr	|- F/_ x TC+ A