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	⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	wceq	⊢ 𝐴 = 𝐵
3		vx	⊢ 𝑥
4		wph	⊢ 𝜑
5	4 3 0	wsbc	⊢ [ 𝐴 / 𝑥 ] 𝜑
6	4 3 1	wsbc	⊢ [ 𝐵 / 𝑥 ] 𝜑
7	5 6	wi	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 )
8	2 7	wi	⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )