Axiom ax_5 ≪ | index | src | ≫

axiom ax_5 (A: wff) {x: set}: $ A \imp \fo x A $;