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

Theorem iunss 4134
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 4097 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3374 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3414 . 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 3339 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2731 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 2976 . . 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 2824 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1576 . . 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 265 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 264 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 178   A.wal 1550    e. wcel 1726   {cab 2424   A.wral 2707   E.wrex 2708    C_ wss 3322   U_ciun 4095
This theorem is referenced by:  iunss2  4138  djussxp  5021  fun11iun  5698  onfununi  6606  oawordeulem  6800  oaabslem  6889  oaabs2  6891  omabslem  6892  omabs  6893  marypha2lem1  7443  trcl  7667  r1val1  7715  rankuni2b  7782  rankval4  7796  rankbnd  7797  rankbnd2  7798  rankc1  7799  cfslb2n  8153  cfsmolem  8155  hsmexlem2  8312  axdc3lem2  8336  ac6  8365  wuncval2  8627  inar1  8655  tskuni  8663  grur1a  8699  wrdexg  11744  prmreclem4  13292  prmreclem5  13293  prdsval  13683  prdsbas  13685  imasaddfnlem  13758  imasaddflem  13760  imasvscafn  13767  imasvscaf  13769  isacs2  13883  mreacs  13888  acsfn  13889  dmcoass  14226  isacs5  14603  dprdspan  15590  dprd2dlem1  15604  dprd2d2  15607  dmdprdsplit2lem  15608  lbsextlem2  16236  lpival  16321  iunocv  16913  tgidm  17050  iuncon  17496  txtube  17677  txcmplem2  17679  xkococnlem  17696  xkoinjcn  17724  alexsubALTlem3  18085  cnextf  18102  imasdsf1olem  18408  metnrmlem3  18896  ovolfiniun  19402  ovoliunlem2  19404  ovoliun  19406  ovoliunnul  19408  volfiniun  19446  voliunlem1  19449  volsup  19455  uniioombllem3a  19481  uniioombllem3  19482  uniioombllem4  19483  ismbf3d  19549  limciun  19786  taylfval  20280  taylf  20282  cvmlift2lem12  25006  rtrclreclem.min  25152  trpredlem1  25510  trpredss  25512  trpredmintr  25514  dftrpred3g  25516  wfrlem7  25549  frrlem5d  25594  frrlem7  25597  nofulllem5  25666  mblfinlem2  26256  volsupnfl  26263  cnambfre  26267  ntruni  26344  comppfsc  26401  neibastop2lem  26403  filnetlem4  26424  sstotbnd2  26497  equivtotbnd  26501  totbndbnd  26512  prdstotbnd  26517  heiborlem1  26534  iunconlem2  29121  bnj226  29175  bnj517  29330  bnj1118  29427  bnj1137  29438  pclfinN  30771  lcfrlem4  32417  lcfrlem16  32430  lcfr  32457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-iun 4097
  Copyright terms: Public domain W3C validator