Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcg | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | ⊢ Ⅎ 𝑥 𝜑 | |
2 | 1 | sbcgf | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) |