Description: Reversed substitution. Version of sb6rf requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993) (Revised by Wolf Lammen, 7-Feb-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sb6rfv.nf | |- F/ y ph |
|
| Assertion | sb6rfv | |- ( ph <-> A. y ( y = x -> [ y / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb6rfv.nf | |- F/ y ph |
|
| 2 | sbequ12r | |- ( y = x -> ( [ y / x ] ph <-> ph ) ) |
|
| 3 | 1 2 | equsalv | |- ( A. y ( y = x -> [ y / x ] ph ) <-> ph ) |
| 4 | 3 | bicomi | |- ( ph <-> A. y ( y = x -> [ y / x ] ph ) ) |