Metamath Proof Explorer


Theorem nfttrcl

Description: Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Hypothesis nfttrcl.1 _xR
Assertion nfttrcl _xt++R

Proof

Step Hyp Ref Expression
1 nfttrcl.1 _xR
2 1 a1i _xR
3 2 nfttrcld _xt++R
4 3 mptru _xt++R