Metamath Proof Explorer

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 -> ( [. A / x ]. ph -> [. B / x ]. ph ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 0 1 wceq 
 |-  A = B
3 vx 
 |-  x
4 wph 
 |-  ph
5 4 3 0 wsbc 
 |-  [. A / x ]. ph
6 4 3 1 wsbc 
 |-  [. B / x ]. ph
7 5 6 wi 
 |-  ( [. A / x ]. ph -> [. B / x ]. ph )
8 2 7 wi 
 |-  ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )