Theorem cnre 7916

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141   E.wrex 2449  (class class class)co 5853   CCcc 7772   RRcr 7773   _ici 7776   + caddc 7777   x. cmul 7779

This theorem was proved from axioms:  ax-cnre 7885

This theorem is referenced by:  mulid1  7917  cnegexlem2  8095  cnegex  8097  apirr  8524  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  apti  8541  recexap  8571  creur  8875  creui  8876  cju  8877  cnref1o  9609  replim  10823  cjap  10870