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

Theorem itgex 22670
 Description: An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.)
Assertion
Ref Expression
itgex

Proof of Theorem itgex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-itg 22523 . 2
2 sumex 13697 . 2
31, 2eqeltri 2502 1
 Colors of variables: wff setvar class Syntax hints:   wa 370   wcel 1872  cvv 3022  csb 3338  cif 3854   class class class wbr 4366   cmpt 4425  cfv 5544  (class class class)co 6249  cr 9489  cc0 9490  ci 9492   cmul 9495   cle 9627   cdiv 10220  c3 10611  cfz 11735  cexp 12222  cre 13104  csu 13695  citg2 22516  citg 22518 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-nul 4498 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-sn 3942  df-pr 3944  df-uni 4163  df-iota 5508  df-sum 13696  df-itg 22523 This theorem is referenced by:  ditgex  22749  ftc1lem1  22929  itgulm  23305  dmarea  23825  dfarea  23828  areaval  23832  ftc1anc  31932  itgsinexp  37714  wallispilem1  37810  wallispilem2  37811
 Copyright terms: Public domain W3C validator