There are the definitions of FV(e) and F̲V̲(e̅::Γ′) on page 27 (Section 1.4.4 Well-formedness) of Mario Carneiro's PhD thesis about Metamath Zero[0]:
FV(x) = {x}
FV_Γ(φ) = x̅ where (φ : s x̅) ∈ Γ
FV(f e̅) = F̲V̲(e̅::Γ′) ∪ {eᵢ | Γ′ᵢ ∈ x̅} where f(Γ′) : s x̅
F̲V̲(·::·) = ∅
F̲V̲((e̅, y)::(Γ′, x : s)) = F̲V̲(e̅::Γ′)
F̲V̲((e̅, e′)::(Γ′, φ : s x̅)) = F̲V̲(e̅::Γ′) ∪ (FV(e′) ∖ {eᵢ | Γ′ᵢ ∈ x̅})
I think {eᵢ | Dom(Γ′ᵢ) ⊆ x̅} should be substituted for {eᵢ | Γ′ᵢ ∈ x̅} in these definitions. Γ′ᵢ is of the form x : s, so Dom(Γ′ᵢ) is of the form {x}.