Theorem cnre 7953

Description: Alias for ax-cnre 7922, 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 7922	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 5875   CCcc 7809   RRcr 7810   _ici 7813   + caddc 7814   x. cmul 7816

This theorem was proved from axioms:  ax-cnre 7922

This theorem is referenced by:  mulrid  7954  cnegexlem2  8133  cnegex  8135  apirr  8562  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  apti  8579  recexap  8610  creur  8916  creui  8917  cju  8918  cnref1o  9650  replim  10868  cjap  10915