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

Theorem iunss2 3921
Description: A subclass condition on the members of two indexed classes 
C ( x ) and  D ( y ) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3832. (Contributed by NM, 9-Dec-2004.)
Assertion
Ref Expression
iunss2  |-  ( A. x  e.  A  E. y  e.  B  C  C_  D  ->  U_ x  e.  A  C  C_  U_ y  e.  B  D )
Distinct variable groups:    x, y    x, B    y, C    x, D
Allowed substitution hints:    A( x, y)    B( y)    C( x)    D( y)

Proof of Theorem iunss2
StepHypRef Expression
1 ssiun 3918 . . 3  |-  ( E. y  e.  B  C  C_  D  ->  C  C_  U_ y  e.  B  D )
21ralimi 2593 . 2  |-  ( A. x  e.  A  E. y  e.  B  C  C_  D  ->  A. x  e.  A  C  C_  U_ y  e.  B  D )
3 iunss 3917 . 2  |-  ( U_ x  e.  A  C  C_ 
U_ y  e.  B  D 
<-> 
A. x  e.  A  C  C_  U_ y  e.  B  D )
42, 3sylibr 205 1  |-  ( A. x  e.  A  E. y  e.  B  C  C_  D  ->  U_ x  e.  A  C  C_  U_ y  e.  B  D )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wral 2518   E.wrex 2519    C_ wss 3127   U_ciun 3879
This theorem is referenced by:  iunxdif2  3924  oaass  6527  odi  6545  omass  6546  oelim2  6561
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ral 2523  df-rex 2524  df-v 2765  df-in 3134  df-ss 3141  df-iun 3881
  Copyright terms: Public domain W3C validator