Theorem frege56c

Description: Lemma for frege57c . Proposition 56 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege56c.b	⊢ 𝐵 ∈ 𝐶
Assertion	frege56c	⊢ ( ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) → ( 𝐵 = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege56c.b	⊢ 𝐵 ∈ 𝐶
2	1	frege54cor1c	⊢ [ 𝐵 / 𝑥 ] 𝑥 = 𝐵
3		frege53c	⊢ ( [ 𝐵 / 𝑥 ] 𝑥 = 𝐵 → ( 𝐵 = 𝐴 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) )
4	2 3	ax-mp	⊢ ( 𝐵 = 𝐴 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 )
5		frege55lem1c	⊢ ( ( 𝐵 = 𝐴 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) → ( 𝐵 = 𝐴 → 𝐴 = 𝐵 ) )
6	4 5	ax-mp	⊢ ( 𝐵 = 𝐴 → 𝐴 = 𝐵 )
7		frege9	⊢ ( ( 𝐵 = 𝐴 → 𝐴 = 𝐵 ) → ( ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) → ( 𝐵 = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) ) )
8	6 7	ax-mp	⊢ ( ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) → ( 𝐵 = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) ) )