Theorem cbvald ≪ | index | src | ≫ 

theorem cbvald {x y: nat} (G: wff) (p: wff x) (q: wff y):
  $ G /\ x = y -> (p <-> q) $ >
  $ G -> (A. x p <-> A. y q) $;
StepHypRefExpression
1 cbvals 
A. x p <-> A. y [y / x] p
2 1 a1i 
G -> (A. x p <-> A. y [y / x] p)
3 sbet 
A. x (x = y -> (p <-> q)) -> ([y / x] p <-> q)
4 hyp h 
G /\ x = y -> (p <-> q)
5 4 ialda 
G -> A. x (x = y -> (p <-> q))
6 3, 5 syl 
G -> ([y / x] p <-> q)
7 6 aleqd 
G -> (A. y [y / x] p <-> A. y q)
8 2, 7 bitrd 
G -> (A. x p <-> A. y q)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12)