Description: If x and y are interchangeable in ph , they are both free or both not free in ph . (Contributed by Wolf Lammen, 6-Aug-2023) (Revised by AV, 23-Sep-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ichnfb | |- ( [ x <> y ] ph -> ( A. x F/ y ph <-> A. y F/ x ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ichcom | |- ( [ x <> y ] ph <-> [ y <> x ] ph ) |
|
| 2 | ichnfim | |- ( ( A. x F/ y ph /\ [ y <> x ] ph ) -> A. y F/ x ph ) |
|
| 3 | 1 2 | sylan2b | |- ( ( A. x F/ y ph /\ [ x <> y ] ph ) -> A. y F/ x ph ) |
| 4 | 3 | expcom | |- ( [ x <> y ] ph -> ( A. x F/ y ph -> A. y F/ x ph ) ) |
| 5 | ichnfim | |- ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. x F/ y ph ) |
|
| 6 | 5 | expcom | |- ( [ x <> y ] ph -> ( A. y F/ x ph -> A. x F/ y ph ) ) |
| 7 | 4 6 | impbid | |- ( [ x <> y ] ph -> ( A. x F/ y ph <-> A. y F/ x ph ) ) |