Metamath Proof Explorer


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