Metamath Proof Explorer

Theorem eufid

Description: Utility theorem: index-independent form of df-euf . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Assertion eufid 
|- EuclF = Slot ( EuclF ` ndx )

Proof

Step Hyp Ref Expression
1 df-euf 
 |-  EuclF = Slot ; 2 1
2 2nn0 
 |-  2 e. NN0
3 1nn 
 |-  1 e. NN
4 2 3 decnncl 
 |-  ; 2 1 e. NN
5 1 4 ndxid 
 |-  EuclF = Slot ( EuclF ` ndx )