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

Theorem excom 1849
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-12 1854, ax-10 1837, ax-6 1747, ax-7 1790 and ax-5 1704. (Revised by Wolf Lammen, 8-Jan-2018.)
Assertion
Ref Expression
excom

Proof of Theorem excom
StepHypRef Expression
1 alcom 1845 . . . 4
21notbii 296 . . 3
3 exnal 1648 . . 3
4 exnal 1648 . . 3
52, 3, 43bitr4i 277 . 2
6 df-ex 1613 . . 3
76exbii 1667 . 2
8 df-ex 1613 . . 3
98exbii 1667 . 2
105, 7, 93bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  A.wal 1393  E.wex 1612
This theorem is referenced by:  excomim  1850  excom13  1851  exrot3  1852  ee4anv  1990  sbel2x  2203  2sb8e  2211  2euex  2366  2eu1OLD  2377  2eu4  2380  2eu4OLD  2381  rexcomf  3017  gencbvex  3153  euind  3286  sbccomlem  3406  opelopabsbALT  4761  elvvv  5064  dmuni  5217  dm0rn0  5224  dmcosseq  5269  elres  5314  rnco  5518  coass  5531  oprabid  6323  dfoprab2  6343  uniuni  6609  opabex3d  6778  opabex3  6779  frxp  6910  domen  7549  xpassen  7631  scott0  8325  dfac5lem1  8525  dfac5lem4  8528  cflem  8647  ltexprlem1  9435  ltexprlem4  9438  fsumcom2  13589  fprodcom2  13788  gsumval3eu  16907  dprd2d2  17093  usgraedg4  24387  cnvoprab  27546  eldm3  29191  dfdm5  29206  dfrn5  29207  elfuns  29565  dfiota3  29573  brimg  29587  brsuccf  29591  funpartlem  29592  sbccom2lem  30529  pm11.6  31298  eliunxp2  32923  ax6e2ndeq  33332  e2ebind  33336  ax6e2ndeqVD  33709  e2ebindVD  33712  e2ebindALT  33729  ax6e2ndeqALT  33731  bj-rexcom4  34445  diblsmopel  36898  dicelval3  36907  dihjatcclem4  37148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-11 1842
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator