Theorem cnre 7948

Description: Alias for ax-cnre 7917, for naming consistency. (Contributed by NM, 3-Jan-2013.)

Assertion

Ref	Expression
cnre	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Distinct variable group:   x, A, y

Proof of Theorem cnre

Step	Hyp	Ref	Expression
1		ax-cnre 7917	1 |- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148   E.wrex 2456  (class class class)co 5870   CCcc 7804   RRcr 7805   _ici 7808   + caddc 7809   x. cmul 7811

This theorem was proved from axioms:  ax-cnre 7917

This theorem is referenced by:  mulrid  7949  cnegexlem2  8127  cnegex  8129  apirr  8556  apsym  8557  apcotr  8558  apadd1  8559  apneg  8562  mulext1  8563  apti  8573  recexap  8604  creur  8910  creui  8911  cju  8912  cnref1o  9644  replim  10859  cjap  10906