Axiom ax-frege52c

Description: One side of dfsbcq . Part of Axiom 52 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege52c	$$⊢A=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wceq	$$wffA=B$$
3		vx	$$setvarx$$
4		wph	$$wff\phi$$
5	4 3 0	wsbc	$$wff\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
6	4 3 1	wsbc	$$wff\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi$$
7	5 6	wi	$$wff\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
8	2 7	wi	$$wff\left(A=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\right)$$