Theorem existene ≪ | index | src | ≫

存在性公理

theorem existene {x: set} (y: set): $ \ex x x = y $;

Step	Hyp	Ref	Expression
1		ax_6	\ex x x = y

Axiom use

Logic (ax_6)