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

Theorem uniprg 4249
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 4095 . . . 4  |-  ( x  =  A  ->  { x ,  y }  =  { A ,  y } )
21unieqd 4245 . . 3  |-  ( x  =  A  ->  U. {
x ,  y }  =  U. { A ,  y } )
3 uneq1 3637 . . 3  |-  ( x  =  A  ->  (
x  u.  y )  =  ( A  u.  y ) )
42, 3eqeq12d 2476 . 2  |-  ( x  =  A  ->  ( U. { x ,  y }  =  ( x  u.  y )  <->  U. { A ,  y }  =  ( A  u.  y
) ) )
5 preq2 4096 . . . 4  |-  ( y  =  B  ->  { A ,  y }  =  { A ,  B }
)
65unieqd 4245 . . 3  |-  ( y  =  B  ->  U. { A ,  y }  =  U. { A ,  B } )
7 uneq2 3638 . . 3  |-  ( y  =  B  ->  ( A  u.  y )  =  ( A  u.  B ) )
86, 7eqeq12d 2476 . 2  |-  ( y  =  B  ->  ( U. { A ,  y }  =  ( A  u.  y )  <->  U. { A ,  B }  =  ( A  u.  B ) ) )
9 vex 3109 . . 3  |-  x  e. 
_V
10 vex 3109 . . 3  |-  y  e. 
_V
119, 10unipr 4248 . 2  |-  U. {
x ,  y }  =  ( x  u.  y )
124, 8, 11vtocl2g 3168 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  U. { A ,  B }  =  ( A  u.  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823    u. cun 3459   {cpr 4018   U.cuni 4235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019  df-uni 4236
This theorem is referenced by:  wunun  9077  tskun  9153  gruun  9173  mrcun  15111  unopn  19579  indistopon  19669  uncon  20096  limcun  22465  sshjval3  26470  prsiga  28361  unelsiga  28364  measxun2  28418  measssd  28423  carsgsigalem  28523  carsgclctun  28529  probun  28622  indispcon  28943  kelac2  31250  fourierdlem70  32198  fourierdlem71  32199
  Copyright terms: Public domain W3C validator