Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | icht.1 | |- ph |
|
Assertion | icht | |- [ x <> y ] ph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | icht.1 | |- ph |
|
2 | 1 | sbt | |- [ a / y ] ph |
3 | 2 | sbt | |- [ y / x ] [ a / y ] ph |
4 | 3 | sbt | |- [ x / a ] [ y / x ] [ a / y ] ph |
5 | 4 1 | 2th | |- ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) |
6 | 5 | gen2 | |- A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) |
7 | df-ich | |- ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) ) |
|
8 | 6 7 | mpbir | |- [ x <> y ] ph |