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

Theorem iunss 4223
Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
iunss  |-  ( U_ x  e.  A  B  C_  C  <->  A. x  e.  A  B  C_  C )
Distinct variable group:    x, C
Allowed substitution hints:    A( x)    B( x)

Proof of Theorem iunss
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-iun 4185 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3392 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3433 . 2  |-  ( { y  |  E. x  e.  A  y  e.  B }  C_  C  <->  A. y
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
4 dfss2 3357 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2751 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3003 . . 3  |-  ( A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C )  <->  A. y A. x  e.  A  ( y  e.  B  ->  y  e.  C ) )
7 r19.23v 2845 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1610 . . 3  |-  ( A. y A. x  e.  A  ( y  e.  B  ->  y  e.  C )  <->  A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
) )
95, 6, 83bitrri 272 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 271 1  |-  ( U_ x  e.  A  B  C_  C  <->  A. x  e.  A  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367    e. wcel 1756   {cab 2429   A.wral 2727   E.wrex 2728    C_ wss 3340   U_ciun 4183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2732  df-rex 2733  df-v 2986  df-in 3347  df-ss 3354  df-iun 4185
This theorem is referenced by:  iunss2  4227  djussxp  4997  fun11iun  6549  onfununi  6814  oawordeulem  7005  oaabslem  7094  oaabs2  7096  omabslem  7097  omabs  7098  marypha2lem1  7697  trcl  7960  r1val1  8005  rankuni2b  8072  rankval4  8086  rankbnd  8087  rankbnd2  8088  rankc1  8089  cfslb2n  8449  cfsmolem  8451  hsmexlem2  8608  axdc3lem2  8632  ac6  8661  wuncval2  8926  inar1  8954  tskuni  8962  grur1a  8998  wrdexg  12256  prmreclem4  13992  prmreclem5  13993  prdsval  14405  prdsbas  14407  imasaddfnlem  14478  imasaddflem  14480  imasvscafn  14487  imasvscaf  14489  isacs2  14603  mreacs  14608  acsfn  14609  dmcoass  14946  isacs5  15354  dprdspan  16536  dprd2dlem1  16552  dprd2d2  16555  dmdprdsplit2lem  16556  lbsextlem2  17252  lpival  17339  iunocv  18118  tgidm  18597  iuncon  19044  txtube  19225  txcmplem2  19227  xkococnlem  19244  xkoinjcn  19272  alexsubALTlem3  19633  cnextf  19650  imasdsf1olem  19960  metnrmlem3  20449  ovolfiniun  20996  ovoliunlem2  20998  ovoliun  21000  ovoliunnul  21002  volfiniun  21040  voliunlem1  21043  volsup  21049  uniioombllem3a  21076  uniioombllem3  21077  uniioombllem4  21078  ismbf3d  21144  limciun  21381  taylfval  21836  taylf  21838  disjunsn  25948  eulerpartlemgh  26773  eulerpartlemgs2  26775  cvmlift2lem12  27215  rtrclreclem.min  27361  trpredlem1  27703  trpredss  27705  trpredmintr  27707  dftrpred3g  27709  wfrlem7  27742  frrlem5d  27787  frrlem7  27790  nofulllem5  27859  mblfinlem2  28441  volsupnfl  28448  cnambfre  28452  ntruni  28534  comppfsc  28591  neibastop2lem  28593  filnetlem4  28614  sstotbnd2  28685  equivtotbnd  28689  totbndbnd  28700  prdstotbnd  28705  heiborlem1  28722  fsuppmapnn0fiublem  30810  fsuppmapnn0fiub  30811  iunconlem2  31683  bnj226  31737  bnj517  31890  bnj1118  31987  bnj1137  31998  pclfinN  33556  lcfrlem4  35202  lcfrlem16  35215  lcfr  35242
  Copyright terms: Public domain W3C validator