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

Theorem uniprg 4206
Description: The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
Assertion
Ref Expression
uniprg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  U. { A ,  B }  =  ( A  u.  B )
)

Proof of Theorem uniprg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq1 4055 . . . 4  |-  ( x  =  A  ->  { x ,  y }  =  { A ,  y } )
21unieqd 4202 . . 3  |-  ( x  =  A  ->  U. {
x ,  y }  =  U. { A ,  y } )
3 uneq1 3604 . . 3  |-  ( x  =  A  ->  (
x  u.  y )  =  ( A  u.  y ) )
42, 3eqeq12d 2473 . 2  |-  ( x  =  A  ->  ( U. { x ,  y }  =  ( x  u.  y )  <->  U. { A ,  y }  =  ( A  u.  y
) ) )
5 preq2 4056 . . . 4  |-  ( y  =  B  ->  { A ,  y }  =  { A ,  B }
)
65unieqd 4202 . . 3  |-  ( y  =  B  ->  U. { A ,  y }  =  U. { A ,  B } )
7 uneq2 3605 . . 3  |-  ( y  =  B  ->  ( A  u.  y )  =  ( A  u.  B ) )
86, 7eqeq12d 2473 . 2  |-  ( y  =  B  ->  ( U. { A ,  y }  =  ( A  u.  y )  <->  U. { A ,  B }  =  ( A  u.  B ) ) )
9 vex 3074 . . 3  |-  x  e. 
_V
10 vex 3074 . . 3  |-  y  e. 
_V
119, 10unipr 4205 . 2  |-  U. {
x ,  y }  =  ( x  u.  y )
124, 8, 11vtocl2g 3133 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  U. { A ,  B }  =  ( A  u.  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758    u. cun 3427   {cpr 3980   U.cuni 4192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-v 3073  df-un 3434  df-sn 3979  df-pr 3981  df-uni 4193
This theorem is referenced by:  wunun  8981  tskun  9057  gruun  9077  mrcun  14671  unopn  18641  indistopon  18730  uncon  19158  limcun  21496  sshjval3  24902  prsiga  26712  unelsiga  26715  measxun2  26762  measssd  26767  probun  26939  indispcon  27260  kelac2  29559
  Copyright terms: Public domain W3C validator