Theorem sbeq1 ≪ | index | src | ≫ 

theorem sbeq1 {x: nat} (a b: nat x) (c: wff x):
  $ a = b -> ([a / x] c <-> [b / x] c) $;
StepHypRefExpression
1 eqeq2 
a = b -> (y = a <-> y = b)
2 1 imeq1d 
a = b -> (y = a -> A. x (x = y -> c) <-> y = b -> A. x (x = y -> c))
3 2 aleqd 
a = b -> (A. y (y = a -> A. x (x = y -> c)) <-> A. y (y = b -> A. x (x = y -> c)))
4 3 conv sb 
a = b -> ([a / x] c <-> [b / x] c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7)