Theorem sbeqd ≪ | index | src | ≫ 

theorem sbeqd (_G: wff) {x: nat} (_a1 _a2: nat x) (_p1 _p2: wff x):
  $ _G -> _a1 = _a2 $ >
  $ _G -> (_p1 <-> _p2) $ >
  $ _G -> ([_a1 / x] _p1 <-> [_a2 / x] _p2) $;
StepHypRefExpression
1 eqidd 
_G -> y = y
2 hyp _ah 
_G -> _a1 = _a2
3 1, 2 eqeqd 
_G -> (y = _a1 <-> y = _a2)
4 biidd 
_G -> (x = y <-> x = y)
5 hyp _ph 
_G -> (_p1 <-> _p2)
6 4, 5 imeqd 
_G -> (x = y -> _p1 <-> x = y -> _p2)
7 6 aleqd 
_G -> (A. x (x = y -> _p1) <-> A. x (x = y -> _p2))
8 3, 7 imeqd 
_G -> (y = _a1 -> A. x (x = y -> _p1) <-> y = _a2 -> A. x (x = y -> _p2))
9 8 aleqd 
_G -> (A. y (y = _a1 -> A. x (x = y -> _p1)) <-> A. y (y = _a2 -> A. x (x = y -> _p2)))
10 9 conv sb 
_G -> ([_a1 / x] _p1 <-> [_a2 / x] _p2)

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)