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 | |- ( A e. V -> ( [. A / x ]. ph <-> ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | |- F/ x ph |
|
2 | 1 | sbcgf | |- ( A e. V -> ( [. A / x ]. ph <-> ph ) ) |