Description: In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BJ and WL, 9-Aug-2023) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sb2ae | |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph <-> [ v / y ] ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drsb1 | |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph <-> [ u / y ] [ v / y ] ph ) ) |
|
2 | nfs1v | |- F/ y [ v / y ] ph |
|
3 | 2 | sbf | |- ( [ u / y ] [ v / y ] ph <-> [ v / y ] ph ) |
4 | 1 3 | bitrdi | |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph <-> [ v / y ] ph ) ) |