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

Theorem unissb 4001
 Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
Assertion
Ref Expression
unissb
Distinct variable groups:   ,   ,

Proof of Theorem unissb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eluni 3974 . . . . . 6
21imbi1i 316 . . . . 5
3 19.23v 1910 . . . . 5
42, 3bitr4i 244 . . . 4
54albii 1572 . . 3
6 alcom 1748 . . . 4
7 19.21v 1909 . . . . . 6
8 impexp 434 . . . . . . . 8
9 bi2.04 351 . . . . . . . 8
108, 9bitri 241 . . . . . . 7
1110albii 1572 . . . . . 6
12 dfss2 3294 . . . . . . 7
1312imbi2i 304 . . . . . 6
147, 11, 133bitr4i 269 . . . . 5
1514albii 1572 . . . 4
166, 15bitri 241 . . 3
175, 16bitri 241 . 2
18 dfss2 3294 . 2
19 df-ral 2668 . 2
2017, 18, 193bitr4i 269 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1546  wex 1547   wcel 1721  wral 2663   wss 3277  cuni 3971 This theorem is referenced by:  uniss2  4002  ssunieq  4004  sspwuni  4131  pwssb  4132  ordunisssuc  4638  bm2.5ii  4740  sorpssuni  6481  sbthlem1  7167  ordunifi  7307  isfinite2  7315  cflim2  8090  fin23lem16  8162  fin23lem29  8168  fin1a2lem11  8237  fin1a2lem13  8239  itunitc  8248  zorng  8331  wuncval2  8569  suplem1pr  8876  suplem2pr  8877  mrcuni  13787  ipodrsfi  14530  mrelatlub  14553  subgint  14905  efgval  15290  toponmre  17098  neips  17118  neiuni  17127  alexsubALTlem2  18018  alexsubALTlem3  18019  tgpconcompeqg  18080  unidmvol  24506  sxbrsigalem0  24543  dya2iocuni  24555  dya2iocucvr  24556  ovoliunnfl  26114  voliunnfl  26116  volsupnfl  26117  topjoin  26246  fnejoin1  26249  fnejoin2  26250  intidl  26491  unichnidl  26493 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ral 2668  df-v 2915  df-in 3284  df-ss 3291  df-uni 3972
 Copyright terms: Public domain W3C validator