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

Theorem iunss 4366
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 4327 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3528 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3569 . 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 3493 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2895 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3132 . . 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 2943 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1620 . . 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 1377    e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815    C_ wss 3476   U_ciun 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327
This theorem is referenced by:  iunss2  4370  djussxp  5148  fun11iun  6744  onfununi  7012  oawordeulem  7203  oaabslem  7292  oaabs2  7294  omabslem  7295  omabs  7296  marypha2lem1  7895  trcl  8159  r1val1  8204  rankuni2b  8271  rankval4  8285  rankbnd  8286  rankbnd2  8287  rankc1  8288  cfslb2n  8648  cfsmolem  8650  hsmexlem2  8807  axdc3lem2  8831  ac6  8860  wuncval2  9125  inar1  9153  tskuni  9161  grur1a  9197  fsuppmapnn0fiublem  12064  fsuppmapnn0fiub  12065  wrdexg  12523  prmreclem4  14296  prmreclem5  14297  prdsval  14710  prdsbas  14712  imasaddfnlem  14783  imasaddflem  14785  imasvscafn  14792  imasvscaf  14794  isacs2  14908  mreacs  14913  acsfn  14914  dmcoass  15251  isacs5  15659  dprdspan  16876  dprd2dlem1  16892  dprd2d2  16895  dmdprdsplit2lem  16896  lbsextlem2  17605  lpival  17692  iunocv  18507  tgidm  19276  iuncon  19723  txtube  19904  txcmplem2  19906  xkococnlem  19923  xkoinjcn  19951  alexsubALTlem3  20312  cnextf  20329  imasdsf1olem  20639  metnrmlem3  21128  ovolfiniun  21675  ovoliunlem2  21677  ovoliun  21679  ovoliunnul  21681  volfiniun  21720  voliunlem1  21723  volsup  21729  uniioombllem3a  21756  uniioombllem3  21757  uniioombllem4  21758  ismbf3d  21824  limciun  22061  taylfval  22516  taylf  22518  disjunsn  27154  eulerpartlemgh  27985  eulerpartlemgs2  27987  cvmlift2lem12  28427  rtrclreclem.min  28573  trpredlem1  28915  trpredss  28917  trpredmintr  28919  dftrpred3g  28921  wfrlem7  28954  frrlem5d  28999  frrlem7  29002  nofulllem5  29071  mblfinlem2  29657  volsupnfl  29664  cnambfre  29668  ntruni  29750  comppfsc  29807  neibastop2lem  29809  filnetlem4  29830  sstotbnd2  29901  equivtotbnd  29905  totbndbnd  29916  prdstotbnd  29921  heiborlem1  29938  iunconlem2  32833  bnj226  32887  bnj517  33040  bnj1118  33137  bnj1137  33148  pclfinN  34714  lcfrlem4  36360  lcfrlem16  36373  lcfr  36400
  Copyright terms: Public domain W3C validator