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

Theorem iunss 4333
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 4294 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3468 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3510 . 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 3433 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2831 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3078 . . 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 2879 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1702 . . 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 280 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 279 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 189   A.wal 1453    e. wcel 1898   {cab 2448   A.wral 2749   E.wrex 2750    C_ wss 3416   U_ciun 4292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-in 3423  df-ss 3430  df-iun 4294
This theorem is referenced by:  iunss2  4337  djussxp  5002  fun11iun  6785  wfrdmss  7073  onfununi  7091  oawordeulem  7286  oaabslem  7375  oaabs2  7377  omabslem  7378  omabs  7379  marypha2lem1  7980  trcl  8243  r1val1  8288  rankuni2b  8355  rankval4  8369  rankbnd  8370  rankbnd2  8371  rankc1  8372  cfslb2n  8729  cfsmolem  8731  hsmexlem2  8888  axdc3lem2  8912  ac6  8941  wuncval2  9203  inar1  9231  tskuni  9239  grur1a  9275  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  wrdexg  12721  rtrclreclem4  13179  prmreclem4  14918  prmreclem5  14919  prdsval  15408  prdsbas  15410  imasaddfnlem  15489  imasaddflem  15491  imasvscafn  15498  imasvscaf  15500  isacs2  15614  mreacs  15619  acsfn  15620  dmcoass  16016  isacs5  16473  dprdspan  17715  dprd2dlem1  17729  dprd2d2  17732  dmdprdsplit2lem  17733  lbsextlem2  18437  lpival  18524  iunocv  19299  tgidm  20051  iuncon  20498  comppfsc  20602  txtube  20710  txcmplem2  20712  xkococnlem  20729  xkoinjcn  20757  alexsubALTlem3  21119  cnextf  21136  imasdsf1olem  21443  metnrmlem3  21933  metnrmlem3OLD  21948  ovolfiniun  22509  ovoliunlem2  22511  ovoliun  22513  ovoliunnul  22515  volfiniun  22556  voliunlem1  22559  volsup  22565  uniioombllem3a  22598  uniioombllem3  22599  uniioombllem4  22600  ismbf3d  22666  limciun  22905  taylfval  23370  taylf  23372  elpwiuncl  28211  disjunsn  28258  esum2d  28965  omssubadd  29178  omssubaddOLD  29182  eulerpartlemgh  29261  eulerpartlemgs2  29263  bnj226  29592  bnj517  29746  bnj1118  29843  bnj1137  29854  cvmlift2lem12  30087  trpredlem1  30518  trpredss  30520  trpredmintr  30522  dftrpred3g  30524  frrlem5d  30571  frrlem7  30574  nofulllem5  30645  ntruni  31033  neibastop2lem  31066  filnetlem4  31087  mblfinlem2  32024  volsupnfl  32031  cnambfre  32035  sstotbnd2  32152  equivtotbnd  32156  totbndbnd  32167  prdstotbnd  32172  heiborlem1  32189  pclfinN  33511  lcfrlem4  35159  lcfrlem16  35172  lcfr  35199  iunrelexp0  36340  iunrelexpmin1  36346  iunrelexpmin2  36350  cotrcltrcl  36363  trclimalb2  36364  cotrclrcl  36380  iunconlem2  37373  ixpssmapc  37457  omeiunle  38446  omeiunltfirp  38448  carageniuncl  38452  caratheodorylem1  38455  caratheodorylem2  38456  hoissrrn  38478  ovnlecvr  38487  ovnsubaddlem1  38499  ovnsubadd  38501  hoissrrn2  38507  ovnlecvr2  38539  hspmbl  38558  opnvonmbllem2  38562  vonvolmbllem  38589  vonvolmbl2  38592  vonvol2  38593
  Copyright terms: Public domain W3C validator