Theorem nfttc

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

	Ref	Expression
Hypothesis	nfttc.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfttc	⊢ Ⅎ 𝑥 TC+ 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfttc.1	⊢ Ⅎ 𝑥 𝐴
2		df-ttc	⊢ TC+ 𝐴 = ∪ 𝑦 ∈ 𝐴 ∪ ( rec ( ( 𝑧 ∈ V ↦ ∪ 𝑧 ) , { 𝑦 } ) “ ω )
3		nfcv	⊢ Ⅎ 𝑥 ∪ ( rec ( ( 𝑧 ∈ V ↦ ∪ 𝑧 ) , { 𝑦 } ) “ ω )
4	1 3	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑦 ∈ 𝐴 ∪ ( rec ( ( 𝑧 ∈ V ↦ ∪ 𝑧 ) , { 𝑦 } ) “ ω )
5	2 4	nfcxfr	⊢ Ⅎ 𝑥 TC+ 𝐴