Metamath Proof Explorer

Theorem cnre

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

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

Proof

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