Description: Substitution applied to the atomic wff with equality. Variant of equsb3 . (Contributed by AV, 29-Jul-2023) (Proof shortened by Wolf Lammen, 2-Sep-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | equsb3r | |- ( [ y / x ] z = x <-> z = y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equequ2 | |- ( x = w -> ( z = x <-> z = w ) ) |
|
| 2 | equequ2 | |- ( w = y -> ( z = w <-> z = y ) ) |
|
| 3 | 1 2 | sbievw2 | |- ( [ y / x ] z = x <-> z = y ) |