Description: A composition law for substitution. Version of sbco2 with disjoint variable conditions but not requiring ax-13 . (Contributed by NM, 30-Jun-1994) (Revised by Wolf Lammen, 29-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbco2v.1 | |- F/ z ph |
|
| Assertion | sbco2v | |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbco2v.1 | |- F/ z ph |
|
| 2 | 1 | nfsbv | |- F/ z [ y / x ] ph |
| 3 | sbequ | |- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) ) |
|
| 4 | 2 3 | sbiev | |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) |