Theorem c0exALT

Description: Alternate proof of c0ex using more set theory axioms but fewer complex number axioms (add ax-10 , ax-11 , ax-13 , ax-nul , and remove ax-1cn , ax-icn , ax-addcl , and ax-mulcl ). (Contributed by Steven Nguyen, 4-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	c0exALT	$$⊢0\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
2	1	eqcomi	$$⊢0=\mathrm{i}\mathrm{i}+1$$
3	2	ovexi	$$⊢0\in \mathrm{V}$$