Metamath Proof Explorer


Theorem frege58c

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 )

Proof

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 )