Description: A weak version of ax-12 which is stronger than ax12v . Note that if one assumes reflexivity of equality |- x = x ( equid ), then bj-ax12v3 implies ax-5 over modal logic K (substitute x for y ). See also bj-ax12v3ALT . (Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ax12v3 | |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | |- ( ph -> A. y ph ) |
|
| 2 | ax12 | |- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) |
|
| 3 | 1 2 | syl5 | |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) |