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

Theorem axcnex 8766
Description: The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 10347), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus we can avoid ax-rep 4134 in later theorems by invoking the axiom ax-cnex 8790 instead of cnexALT 10347. (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 8740 . 2  |-  CC  =  ( R.  X.  R. )
2 df-nr 8679 . . . 4  |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
3 npex 8607 . . . . . . 7  |-  P.  e.  _V
43, 3xpex 4802 . . . . . 6  |-  ( P. 
X.  P. )  e.  _V
54pwex 4194 . . . . 5  |-  ~P ( P.  X.  P. )  e. 
_V
6 enrer 8687 . . . . . . . 8  |-  ~R  Er  ( P.  X.  P. )
76a1i 12 . . . . . . 7  |-  (  T. 
->  ~R  Er  ( P. 
X.  P. ) )
87qsss 6717 . . . . . 6  |-  (  T. 
->  ( ( P.  X.  P. ) /.  ~R  )  C_ 
~P ( P.  X.  P. ) )
98trud 1316 . . . . 5  |-  ( ( P.  X.  P. ) /.  ~R  )  C_  ~P ( P.  X.  P. )
105, 9ssexi 4162 . . . 4  |-  ( ( P.  X.  P. ) /.  ~R  )  e.  _V
112, 10eqeltri 2356 . . 3  |-  R.  e.  _V
1211, 11xpex 4802 . 2  |-  ( R. 
X.  R. )  e.  _V
131, 12eqeltri 2356 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    T. wtru 1309    e. wcel 1687   _Vcvv 2791    C_ wss 3155   ~Pcpw 3628    X. cxp 4688    Er wer 6654   /.cqs 6656   P.cnp 8478    ~R cer 8485   R.cnr 8486   CCcc 8732
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-inf2 7339
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-reu 2553  df-rmo 2554  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-uni 3831  df-int 3866  df-iun 3910  df-br 4027  df-opab 4081  df-mpt 4082  df-tr 4117  df-eprel 4306  df-id 4310  df-po 4315  df-so 4316  df-fr 4353  df-we 4355  df-ord 4396  df-on 4397  df-lim 4398  df-suc 4399  df-om 4658  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-1st 6085  df-2nd 6086  df-recs 6385  df-rdg 6420  df-1o 6476  df-oadd 6480  df-omul 6481  df-er 6657  df-ec 6659  df-qs 6663  df-ni 8493  df-pli 8494  df-mi 8495  df-lti 8496  df-plpq 8529  df-mpq 8530  df-ltpq 8531  df-enq 8532  df-nq 8533  df-erq 8534  df-plq 8535  df-mq 8536  df-1nq 8537  df-rq 8538  df-ltnq 8539  df-np 8602  df-plp 8604  df-ltp 8606  df-enr 8678  df-nr 8679  df-c 8740
  Copyright terms: Public domain W3C validator