Theorem cnre 7853

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 2125   E.wrex 2433  (class class class)co 5814   CCcc 7709   RRcr 7710   _ici 7713   + caddc 7714   x. cmul 7716

This theorem was proved from axioms:  ax-cnre 7822

This theorem is referenced by:  mulid1  7854  cnegexlem2  8030  cnegex  8032  apirr  8459  apsym  8460  apcotr  8461  apadd1  8462  apneg  8465  mulext1  8466  apti  8476  recexap  8506  creur  8809  creui  8810  cju  8811  cnref1o  9537  replim  10736  cjap  10783