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 e. _V

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	|- ( ( _i x. _i ) + 1 ) = 0
2	1	eqcomi	|- 0 = ( ( _i x. _i ) + 1 )
3	2	ovexi	|- 0 e. _V