Theorem intro_fo ≪ | index | src | ≫

\fo引入

theorem intro_fo {x: set} (A: wff x): $ A $ > $ \fo x A $;
StepHypRefExpression
1 hyp h 
A
2 1 ax_gen 
\fo x A

Axiom use

Logic (ax_gen)