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

Theorem unissb 4232
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  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
Distinct variable groups:    x, A    x, B

Proof of Theorem unissb
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eluni 4203 . . . . . 6  |-  ( y  e.  U. A  <->  E. x
( y  e.  x  /\  x  e.  A
) )
21imbi1i 325 . . . . 5  |-  ( ( y  e.  U. A  ->  y  e.  B )  <-> 
( E. x ( y  e.  x  /\  x  e.  A )  ->  y  e.  B ) )
3 19.23v 1922 . . . . 5  |-  ( A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  ( E. x ( y  e.  x  /\  x  e.  A )  ->  y  e.  B ) )
42, 3bitr4i 252 . . . 4  |-  ( ( y  e.  U. A  ->  y  e.  B )  <->  A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B ) )
54albii 1611 . . 3  |-  ( A. y ( y  e. 
U. A  ->  y  e.  B )  <->  A. y A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B ) )
6 alcom 1785 . . . 4  |-  ( A. y A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  A. x A. y ( ( y  e.  x  /\  x  e.  A
)  ->  y  e.  B ) )
7 19.21v 1921 . . . . . 6  |-  ( A. y ( x  e.  A  ->  ( y  e.  x  ->  y  e.  B ) )  <->  ( x  e.  A  ->  A. y
( y  e.  x  ->  y  e.  B ) ) )
8 impexp 446 . . . . . . . 8  |-  ( ( ( y  e.  x  /\  x  e.  A
)  ->  y  e.  B )  <->  ( y  e.  x  ->  ( x  e.  A  ->  y  e.  B ) ) )
9 bi2.04 361 . . . . . . . 8  |-  ( ( y  e.  x  -> 
( x  e.  A  ->  y  e.  B ) )  <->  ( x  e.  A  ->  ( y  e.  x  ->  y  e.  B ) ) )
108, 9bitri 249 . . . . . . 7  |-  ( ( ( y  e.  x  /\  x  e.  A
)  ->  y  e.  B )  <->  ( x  e.  A  ->  ( y  e.  x  ->  y  e.  B ) ) )
1110albii 1611 . . . . . 6  |-  ( A. y ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  A. y
( x  e.  A  ->  ( y  e.  x  ->  y  e.  B ) ) )
12 dfss2 3454 . . . . . . 7  |-  ( x 
C_  B  <->  A. y
( y  e.  x  ->  y  e.  B ) )
1312imbi2i 312 . . . . . 6  |-  ( ( x  e.  A  ->  x  C_  B )  <->  ( x  e.  A  ->  A. y
( y  e.  x  ->  y  e.  B ) ) )
147, 11, 133bitr4i 277 . . . . 5  |-  ( A. y ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  ( x  e.  A  ->  x  C_  B ) )
1514albii 1611 . . . 4  |-  ( A. x A. y ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  A. x ( x  e.  A  ->  x  C_  B
) )
166, 15bitri 249 . . 3  |-  ( A. y A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  B )  <->  A. x ( x  e.  A  ->  x  C_  B
) )
175, 16bitri 249 . 2  |-  ( A. y ( y  e. 
U. A  ->  y  e.  B )  <->  A. x
( x  e.  A  ->  x  C_  B )
)
18 dfss2 3454 . 2  |-  ( U. A  C_  B  <->  A. y
( y  e.  U. A  ->  y  e.  B
) )
19 df-ral 2804 . 2  |-  ( A. x  e.  A  x  C_  B  <->  A. x ( x  e.  A  ->  x  C_  B ) )
2017, 18, 193bitr4i 277 1  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1368   E.wex 1587    e. wcel 1758   A.wral 2799    C_ wss 3437   U.cuni 4200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-in 3444  df-ss 3451  df-uni 4201
This theorem is referenced by:  uniss2  4233  ssunieq  4235  sspwuni  4365  pwssb  4366  ordunisssuc  4930  sorpssuni  6480  bm2.5ii  6528  sbthlem1  7532  ordunifi  7674  isfinite2  7682  cflim2  8544  fin23lem16  8616  fin23lem29  8622  fin1a2lem11  8691  fin1a2lem13  8693  itunitc  8702  zorng  8785  wuncval2  9026  suplem1pr  9333  suplem2pr  9334  mrcuni  14679  ipodrsfi  15453  mrelatlub  15476  subgint  15825  efgval  16336  toponmre  18830  neips  18850  neiuni  18859  alexsubALTlem2  19753  alexsubALTlem3  19754  tgpconcompeqg  19815  tglnunirn  23119  unidmvol  26789  sxbrsigalem0  26831  dya2iocuni  26843  dya2iocucvr  26844  ovoliunnfl  28582  voliunnfl  28584  volsupnfl  28585  topjoin  28735  fnejoin1  28738  fnejoin2  28739  intidl  28978  unichnidl  28980
  Copyright terms: Public domain W3C validator