MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcnex Unicode version

Theorem axcnex 8646
Description: The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 10196), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus we can avoid ax-rep 4025 in later theorems by invoking the axiom ax-cnex 8670 instead of cnexALT 10196. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
Assertion
Ref Expression
axcnex  |-  CC  e.  _V

Proof of Theorem axcnex
StepHypRef Expression
1 df-c 8620 . 2  |-  CC  =  ( R.  X.  R. )
2 df-nr 8559 . . . 4  |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
3 npex 8487 . . . . . . 7  |-  P.  e.  _V
43, 3xpex 4705 . . . . . 6  |-  ( P. 
X.  P. )  e.  _V
54pwex 4084 . . . . 5  |-  ~P ( P.  X.  P. )  e. 
_V
6 enrer 8567 . . . . . . . 8  |-  ~R  Er  ( P.  X.  P. )
76a1i 12 . . . . . . 7  |-  (  T. 
->  ~R  Er  ( P. 
X.  P. ) )
87qsss 6603 . . . . . 6  |-  (  T. 
->  ( ( P.  X.  P. ) /.  ~R  )  C_ 
~P ( P.  X.  P. ) )
98trud 1320 . . . . 5  |-  ( ( P.  X.  P. ) /.  ~R  )  C_  ~P ( P.  X.  P. )
105, 9ssexi 4053 . . . 4  |-  ( ( P.  X.  P. ) /.  ~R  )  e.  _V
112, 10eqeltri 2323 . . 3  |-  R.  e.  _V
1211, 11xpex 4705 . 2  |-  ( R. 
X.  R. )  e.  _V
131, 12eqeltri 2323 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    T. wtru 1312    e. wcel 1621   _Vcvv 2725    C_ wss 3075   ~Pcpw 3527    X. cxp 4575    Er wer 6540   /.cqs 6542   P.cnp 8358    ~R cer 8365   R.cnr 8366   CCcc 8612
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pow 4079  ax-pr 4105  ax-un 4400  ax-inf2 7223
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-reu 2513  df-rab 2514  df-v 2727  df-sbc 2920  df-csb 3007  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-pss 3088  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-tp 3549  df-op 3550  df-uni 3725  df-int 3758  df-iun 3802  df-br 3918  df-opab 3972  df-mpt 3973  df-tr 4008  df-eprel 4195  df-id 4199  df-po 4204  df-so 4205  df-fr 4242  df-we 4244  df-ord 4285  df-on 4286  df-lim 4287  df-suc 4288  df-om 4545  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fun 4599  df-fn 4600  df-f 4601  df-f1 4602  df-fo 4603  df-f1o 4604  df-fv 4605  df-ov 5710  df-oprab 5711  df-mpt2 5712  df-1st 5971  df-2nd 5972  df-recs 6271  df-rdg 6306  df-1o 6362  df-oadd 6366  df-omul 6367  df-er 6543  df-ec 6545  df-qs 6549  df-ni 8373  df-pli 8374  df-mi 8375  df-lti 8376  df-plpq 8409  df-mpq 8410  df-ltpq 8411  df-enq 8412  df-nq 8413  df-erq 8414  df-plq 8415  df-mq 8416  df-1nq 8417  df-rq 8418  df-ltnq 8419  df-np 8482  df-plp 8484  df-ltp 8486  df-enr 8558  df-nr 8559  df-c 8620
  Copyright terms: Public domain W3C validator