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

Theorem unissb 4281
 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 4252 . . . . . 6
21imbi1i 325 . . . . 5
3 19.23v 1760 . . . . 5
42, 3bitr4i 252 . . . 4
54albii 1640 . . 3
6 alcom 1845 . . . 4
7 19.21v 1729 . . . . . 6
8 impexp 446 . . . . . . . 8
9 bi2.04 361 . . . . . . . 8
108, 9bitri 249 . . . . . . 7
1110albii 1640 . . . . . 6
12 dfss2 3492 . . . . . . 7
1312imbi2i 312 . . . . . 6
147, 11, 133bitr4i 277 . . . . 5
1514albii 1640 . . . 4
166, 15bitri 249 . . 3
175, 16bitri 249 . 2
18 dfss2 3492 . 2
19 df-ral 2812 . 2
2017, 18, 193bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  e.wcel 1818  A.wral 2807  C_wss 3475  U.cuni 4249 This theorem is referenced by:  uniss2  4282  ssunieq  4284  sspwuni  4416  pwssb  4417  ordunisssuc  4985  sorpssuni  6589  bm2.5ii  6641  sbthlem1  7647  ordunifi  7790  isfinite2  7798  cflim2  8664  fin23lem16  8736  fin23lem29  8742  fin1a2lem11  8811  fin1a2lem13  8813  itunitc  8822  zorng  8905  wuncval2  9146  suplem1pr  9451  suplem2pr  9452  mrcuni  15018  ipodrsfi  15793  mrelatlub  15816  subgint  16225  efgval  16735  toponmre  19594  neips  19614  neiuni  19623  alexsubALTlem2  20548  alexsubALTlem3  20549  tgpconcompeqg  20610  tglnunirn  23935  uniinn0  27424  locfinreflem  27843  unidmvol  28200  sxbrsigalem0  28242  dya2iocuni  28254  dya2iocucvr  28255  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  topjoin  30183  fnejoin1  30186  fnejoin2  30187  intidl  30426  unichnidl  30428 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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250
 Copyright terms: Public domain W3C validator