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

Theorem iunss 4340
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 4301 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3488 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3530 . 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 3453 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2853 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3100 . . 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 2902 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1685 . . 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 275 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 274 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 187   A.wal 1435    e. wcel 1872   {cab 2407   A.wral 2771   E.wrex 2772    C_ wss 3436   U_ciun 4299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-v 3082  df-in 3443  df-ss 3450  df-iun 4301
This theorem is referenced by:  iunss2  4344  djussxp  4999  fun11iun  6768  wfrdmss  7054  onfununi  7072  oawordeulem  7267  oaabslem  7356  oaabs2  7358  omabslem  7359  omabs  7360  marypha2lem1  7959  trcl  8221  r1val1  8266  rankuni2b  8333  rankval4  8347  rankbnd  8348  rankbnd2  8349  rankc1  8350  cfslb2n  8706  cfsmolem  8708  hsmexlem2  8865  axdc3lem2  8889  ac6  8918  wuncval2  9180  inar1  9208  tskuni  9216  grur1a  9252  fsuppmapnn0fiublem  12209  fsuppmapnn0fiub  12210  wrdexg  12687  rtrclreclem4  13125  prmreclem4  14863  prmreclem5  14864  prdsval  15353  prdsbas  15355  imasaddfnlem  15434  imasaddflem  15436  imasvscafn  15443  imasvscaf  15445  isacs2  15559  mreacs  15564  acsfn  15565  dmcoass  15961  isacs5  16418  dprdspan  17660  dprd2dlem1  17674  dprd2d2  17677  dmdprdsplit2lem  17678  lbsextlem2  18382  lpival  18469  iunocv  19243  tgidm  19995  iuncon  20442  comppfsc  20546  txtube  20654  txcmplem2  20656  xkococnlem  20673  xkoinjcn  20701  alexsubALTlem3  21063  cnextf  21080  imasdsf1olem  21387  metnrmlem3  21877  metnrmlem3OLD  21892  ovolfiniun  22453  ovoliunlem2  22455  ovoliun  22457  ovoliunnul  22459  volfiniun  22499  voliunlem1  22502  volsup  22508  uniioombllem3a  22541  uniioombllem3  22542  uniioombllem4  22543  ismbf3d  22609  limciun  22848  taylfval  23313  taylf  23315  elpwiuncl  28158  disjunsn  28207  esum2d  28923  omssubadd  29137  omssubaddOLD  29141  eulerpartlemgh  29220  eulerpartlemgs2  29222  bnj226  29551  bnj517  29705  bnj1118  29802  bnj1137  29813  cvmlift2lem12  30046  trpredlem1  30476  trpredss  30478  trpredmintr  30480  dftrpred3g  30482  frrlem5d  30529  frrlem7  30532  nofulllem5  30601  ntruni  30989  neibastop2lem  31022  filnetlem4  31043  mblfinlem2  31943  volsupnfl  31950  cnambfre  31954  sstotbnd2  32071  equivtotbnd  32075  totbndbnd  32086  prdstotbnd  32091  heiborlem1  32108  pclfinN  33435  lcfrlem4  35083  lcfrlem16  35096  lcfr  35123  iunrelexp0  36265  iunrelexpmin1  36271  iunrelexpmin2  36275  cotrcltrcl  36288  trclimalb2  36289  cotrclrcl  36305  iunconlem2  37306  omeiunle  38247  omeiunltfirp  38249  carageniuncl  38253  caratheodorylem1  38256  caratheodorylem2  38257  hoissrrn  38276  ovnlecvr  38285  ovnsubaddlem1  38297  ovnsubadd  38299  hoissrrn2  38305
  Copyright terms: Public domain W3C validator