Description: Principle related to sp . Axiom 58 of Frege1879 p. 51. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frege58c.a | |- A e. B |
|
Assertion | frege58c | |- ( A. x ph -> [. A / x ]. ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege58c.a | |- A e. B |
|
2 | ax-frege58b | |- ( A. x ph -> [ y / x ] ph ) |
|
3 | sbsbc | |- ( [ y / x ] ph <-> [. y / x ]. ph ) |
|
4 | 2 3 | sylib | |- ( A. x ph -> [. y / x ]. ph ) |
5 | dfsbcq | |- ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) ) |
|
6 | 4 5 | syl5ib | |- ( y = A -> ( A. x ph -> [. A / x ]. ph ) ) |
7 | 6 | vtocleg | |- ( A e. B -> ( A. x ph -> [. A / x ]. ph ) ) |
8 | 1 7 | ax-mp | |- ( A. x ph -> [. A / x ]. ph ) |