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

Theorem iunss 4024
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 3988 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3278 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3318 . 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 3245 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2643 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 2882 . . 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 2735 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1566 . . 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 263 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 262 1  |-  ( U_ x  e.  A  B  C_  C  <->  A. x  e.  A  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1540    e. wcel 1710   {cab 2344   A.wral 2619   E.wrex 2620    C_ wss 3228   U_ciun 3986
This theorem is referenced by:  iunss2  4028  djussxp  4911  fun11iun  5576  onfununi  6445  oawordeulem  6639  oaabslem  6728  oaabs2  6730  omabslem  6731  omabs  6732  marypha2lem1  7278  trcl  7500  r1val1  7548  rankuni2b  7615  rankval4  7629  rankbnd  7630  rankbnd2  7631  rankc1  7632  cfslb2n  7984  cfsmolem  7986  hsmexlem2  8143  axdc3lem2  8167  ac6  8197  wuncval2  8459  inar1  8487  tskuni  8495  grur1a  8531  wrdexg  11521  prmreclem4  13063  prmreclem5  13064  prdsval  13454  prdsbas  13456  imasaddfnlem  13529  imasaddflem  13531  imasvscafn  13538  imasvscaf  13540  isacs2  13654  mreacs  13659  acsfn  13660  dmcoass  13997  isacs5  14374  dprdspan  15361  dprd2dlem1  15375  dprd2d2  15378  dmdprdsplit2lem  15379  lbsextlem2  16011  lpival  16096  iunocv  16687  tgidm  16824  iuncon  17260  txtube  17440  txcmplem2  17442  xkococnlem  17459  xkoinjcn  17487  alexsubALTlem3  17845  imasdsf1olem  18039  metnrmlem3  18468  ovolfiniun  18964  ovoliunlem2  18966  ovoliun  18968  ovoliunnul  18970  volfiniun  19008  voliunlem1  19011  volsup  19017  uniioombllem3a  19043  uniioombllem3  19044  uniioombllem4  19045  ismbf3d  19113  limciun  19348  taylfval  19842  taylf  19844  cnextf  23503  cvmlift2lem12  24249  rtrclreclem.min  24448  trpredlem1  24788  trpredss  24790  trpredmintr  24792  dftrpred3g  24794  wfrlem7  24820  frrlem5d  24846  frrlem7  24849  nofulllem5  24918  volsupnfl  25491  ntruni  25569  comppfsc  25631  neibastop2lem  25633  filnetlem4  25654  sstotbnd2  25821  equivtotbnd  25825  totbndbnd  25836  prdstotbnd  25841  heiborlem1  25858  bnj226  28524  bnj517  28679  bnj1118  28776  bnj1137  28787  pclfinN  30158  lcfrlem4  31804  lcfrlem16  31817  lcfr  31844
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-v 2866  df-in 3235  df-ss 3242  df-iun 3988
  Copyright terms: Public domain W3C validator