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

Theorem 19.43 1693
Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.43

Proof of Theorem 19.43
StepHypRef Expression
1 df-or 370 . . . 4
21exbii 1667 . . 3
3 19.35 1687 . . 3
4 alnex 1614 . . . 4
54imbi1i 325 . . 3
62, 3, 53bitri 271 . 2
7 df-or 370 . 2
86, 7bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  A.wal 1393  E.wex 1612
This theorem is referenced by:  19.34  1759  19.44v  1770  19.44  1969  19.45  1970  rexun  3683  unipr  4262  uniun  4268  unopab  4527  zfpair  4689  dmun  5214  coundi  5513  coundir  5514  kmlem16  8566  vdwapun  14492  usgraedg4  24387  pm10.42  31269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-or 370  df-ex 1613
  Copyright terms: Public domain W3C validator