Metamath Proof Explorer


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 𝐴𝐵
Assertion frege58c ( ∀ 𝑥 𝜑[ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 frege58c.a 𝐴𝐵
2 ax-frege58b ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
3 sbsbc ( [ 𝑦 / 𝑥 ] 𝜑[ 𝑦 / 𝑥 ] 𝜑 )
4 2 3 sylib ( ∀ 𝑥 𝜑[ 𝑦 / 𝑥 ] 𝜑 )
5 dfsbcq ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜑 ) )
6 4 5 syl5ib ( 𝑦 = 𝐴 → ( ∀ 𝑥 𝜑[ 𝐴 / 𝑥 ] 𝜑 ) )
7 6 vtocleg ( 𝐴𝐵 → ( ∀ 𝑥 𝜑[ 𝐴 / 𝑥 ] 𝜑 ) )
8 1 7 ax-mp ( ∀ 𝑥 𝜑[ 𝐴 / 𝑥 ] 𝜑 )