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

Theorem iunss 4343
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 4304 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3494 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3536 . 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 3459 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2863 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3106 . . 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 2912 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1687 . . 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 1870   {cab 2414   A.wral 2782   E.wrex 2783    C_ wss 3442   U_ciun 4302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-in 3449  df-ss 3456  df-iun 4304
This theorem is referenced by:  iunss2  4347  djussxp  5000  fun11iun  6767  wfrdmss  7050  onfununi  7068  oawordeulem  7263  oaabslem  7352  oaabs2  7354  omabslem  7355  omabs  7356  marypha2lem1  7955  trcl  8211  r1val1  8256  rankuni2b  8323  rankval4  8337  rankbnd  8338  rankbnd2  8339  rankc1  8340  cfslb2n  8696  cfsmolem  8698  hsmexlem2  8855  axdc3lem2  8879  ac6  8908  wuncval2  9171  inar1  9199  tskuni  9207  grur1a  9243  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  wrdexg  12669  rtrclreclem4  13103  prmreclem4  14826  prmreclem5  14827  prdsval  15312  prdsbas  15314  imasaddfnlem  15385  imasaddflem  15387  imasvscafn  15394  imasvscaf  15396  isacs2  15510  mreacs  15515  acsfn  15516  dmcoass  15912  isacs5  16369  dprdspan  17595  dprd2dlem1  17609  dprd2d2  17612  dmdprdsplit2lem  17613  lbsextlem2  18317  lpival  18404  iunocv  19175  tgidm  19927  iuncon  20374  comppfsc  20478  txtube  20586  txcmplem2  20588  xkococnlem  20605  xkoinjcn  20633  alexsubALTlem3  20995  cnextf  21012  imasdsf1olem  21319  metnrmlem3  21789  ovolfiniun  22332  ovoliunlem2  22334  ovoliun  22336  ovoliunnul  22338  volfiniun  22377  voliunlem1  22380  volsup  22386  uniioombllem3a  22419  uniioombllem3  22420  uniioombllem4  22421  ismbf3d  22487  limciun  22726  taylfval  23179  taylf  23181  elpwiuncl  27994  disjunsn  28043  esum2d  28753  omssubadd  28961  eulerpartlemgh  29037  eulerpartlemgs2  29039  bnj226  29330  bnj517  29484  bnj1118  29581  bnj1137  29592  cvmlift2lem12  29825  trpredlem1  30255  trpredss  30257  trpredmintr  30259  dftrpred3g  30261  frrlem5d  30308  frrlem7  30311  nofulllem5  30380  ntruni  30768  neibastop2lem  30801  filnetlem4  30822  mblfinlem2  31682  volsupnfl  31689  cnambfre  31693  sstotbnd2  31810  equivtotbnd  31814  totbndbnd  31825  prdstotbnd  31830  heiborlem1  31847  pclfinN  33174  lcfrlem4  34822  lcfrlem16  34835  lcfr  34862  iunrelexp0  35933  iunrelexpmin1  35939  iunrelexpmin2  35943  cotrcltrcl  35956  trclimalb2  35957  cotrclrcl  35973  iunconlem2  36972  omeiunle  37847  omeiunltfirp  37849  carageniuncl  37853  caratheodorylem1  37856  caratheodorylem2  37857
  Copyright terms: Public domain W3C validator