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 ∈ V

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
2	1	eqcomi	⊢ 0 = ( ( i · i ) + 1 )
3	2	ovexi	⊢ 0 ∈ V