Theorem fo_intro_abs ≪ | index | src | ≫

\fo无关引入

theorem fo_intro_abs (A: wff) {x: set}: $ A \imp \fo x A $;

Step	Hyp	Ref	Expression
1		ax_5	A \imp \fo x A

Axiom use

Logic (ax_5)