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\in B$$
Assertion	frege58c	$$⊢\forall x\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		frege58c.a	$$⊢A\in B$$
2		ax-frege58b	$$⊢\forall x\phi \to \left[y/x\right]\phi$$
3		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
4	2 3	sylib	$$⊢\forall x\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
5		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
6	4 5	syl5ib	$$⊢y=A\to \left(\forall x\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
7	6	vtocleg	$$⊢A\in B\to \left(\forall x\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
8	1 7	ax-mp	$$⊢\forall x\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$