Theorem cnre 7484

Description: Alias for ax-cnre 7456, 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 7456	1 |- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Syntax hints:   -> wi 4   = wceq 1289   e. wcel 1438   E.wrex 2360  (class class class)co 5652   CCcc 7348   RRcr 7349   _ici 7352   + caddc 7353   x. cmul 7355

This theorem was proved from axioms:  ax-cnre 7456

This theorem is referenced by:  mulid1  7485  cnegexlem2  7658  cnegex  7660  apirr  8082  apsym  8083  apcotr  8084  apadd1  8085  apneg  8088  mulext1  8089  apti  8099  recexap  8122  creur  8419  creui  8420  cju  8421  cnref1o  9133  replim  10293  cjap  10340