Theorem intro_sb ≪ | index | src | ≫

如果A可证，则A中任意变量替换后也可证。

theorem intro_sb {x: set} (y: set) (A: wff x): $ A $ > $ \sb y x A $;
StepHypRefExpression
1 fo_elim_sb 
\fo x A \imp \sb y x A
2 hyp h 
A
3 2 intro_fo 
\fo x A
4 1, 3 ax_mp 
\sb y x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)