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	imbitrid	|- ( 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 )