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

Theorem iunss 4373
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 4334 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3523 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3565 . 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 3488 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2888 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 3128 . . 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 2937 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1641 . . 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 272 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 271 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 184   A.wal 1393    e. wcel 1819   {cab 2442   A.wral 2807   E.wrex 2808    C_ wss 3471   U_ciun 4332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3478  df-ss 3485  df-iun 4334
This theorem is referenced by:  iunss2  4377  djussxp  5158  fun11iun  6759  onfununi  7030  oawordeulem  7221  oaabslem  7310  oaabs2  7312  omabslem  7313  omabs  7314  marypha2lem1  7913  trcl  8176  r1val1  8221  rankuni2b  8288  rankval4  8302  rankbnd  8303  rankbnd2  8304  rankc1  8305  cfslb2n  8665  cfsmolem  8667  hsmexlem2  8824  axdc3lem2  8848  ac6  8877  wuncval2  9142  inar1  9170  tskuni  9178  grur1a  9214  fsuppmapnn0fiublem  12099  fsuppmapnn0fiub  12100  wrdexg  12564  prmreclem4  14449  prmreclem5  14450  prdsval  14872  prdsbas  14874  imasaddfnlem  14945  imasaddflem  14947  imasvscafn  14954  imasvscaf  14956  isacs2  15070  mreacs  15075  acsfn  15076  dmcoass  15472  isacs5  15929  dprdspan  17201  dprd2dlem1  17217  dprd2d2  17220  dmdprdsplit2lem  17221  lbsextlem2  17932  lpival  18020  iunocv  18839  tgidm  19609  iuncon  20055  comppfsc  20159  txtube  20267  txcmplem2  20269  xkococnlem  20286  xkoinjcn  20314  alexsubALTlem3  20675  cnextf  20692  imasdsf1olem  21002  metnrmlem3  21491  ovolfiniun  22038  ovoliunlem2  22040  ovoliun  22042  ovoliunnul  22044  volfiniun  22083  voliunlem1  22086  volsup  22092  uniioombllem3a  22119  uniioombllem3  22120  uniioombllem4  22121  ismbf3d  22187  limciun  22424  taylfval  22880  taylf  22882  elpwiuncl  27551  disjunsn  27593  esum2d  28265  omssubadd  28444  eulerpartlemgh  28514  eulerpartlemgs2  28516  cvmlift2lem12  28956  rtrclreclem.min  29267  trpredlem1  29506  trpredss  29508  trpredmintr  29510  dftrpred3g  29512  wfrlem7  29545  frrlem5d  29590  frrlem7  29593  nofulllem5  29662  mblfinlem2  30236  volsupnfl  30243  cnambfre  30247  ntruni  30329  neibastop2lem  30362  filnetlem4  30383  sstotbnd2  30454  equivtotbnd  30458  totbndbnd  30469  prdstotbnd  30474  heiborlem1  30491  iunconlem2  33857  bnj226  33911  bnj517  34065  bnj1118  34162  bnj1137  34173  pclfinN  35746  lcfrlem4  37394  lcfrlem16  37407  lcfr  37434
  Copyright terms: Public domain W3C validator