MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addex Structured version   Visualization version   GIF version

Theorem addex 12969
Description: The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
addex + ∈ V

Proof of Theorem addex
StepHypRef Expression
1 ax-addf 11185 . 2 + :(ℂ × ℂ)⟶ℂ
2 cnex 11187 . . 3 ℂ ∈ V
32, 2xpex 7733 . 2 (ℂ × ℂ) ∈ V
4 fex2 7917 . 2 (( + :(ℂ × ℂ)⟶ℂ ∧ (ℂ × ℂ) ∈ V ∧ ℂ ∈ V) → + ∈ V)
51, 3, 2, 4mp3an 1457 1 + ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2098  Vcvv 3466   × cxp 5664  wf 6529  cc 11104   + caddc 11109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-xp 5672  df-rel 5673  df-cnv 5674  df-dm 5676  df-rn 5677  df-fun 6535  df-fn 6536  df-f 6537
This theorem is referenced by:  cnaddablx  19778  cnaddabl  19779  cnaddid  19780  cnaddinv  19781  zaddablx  19782  cnfldadd  21233  cnfldfun  21240  cnfldfunALT  21241  cnfldfunALTOLD  21242  cnlmodlem2  24986  cnnvg  30400  cnnvs  30402  cncph  30541  cnaddcom  38332  nn0mnd  47042
  Copyright terms: Public domain W3C validator