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

Theorem uniprg 4204
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 4042 . . . 4  |-  ( x  =  A  ->  { x ,  y }  =  { A ,  y } )
21unieqd 4200 . . 3  |-  ( x  =  A  ->  U. {
x ,  y }  =  U. { A ,  y } )
3 uneq1 3572 . . 3  |-  ( x  =  A  ->  (
x  u.  y )  =  ( A  u.  y ) )
42, 3eqeq12d 2486 . 2  |-  ( x  =  A  ->  ( U. { x ,  y }  =  ( x  u.  y )  <->  U. { A ,  y }  =  ( A  u.  y
) ) )
5 preq2 4043 . . . 4  |-  ( y  =  B  ->  { A ,  y }  =  { A ,  B }
)
65unieqd 4200 . . 3  |-  ( y  =  B  ->  U. { A ,  y }  =  U. { A ,  B } )
7 uneq2 3573 . . 3  |-  ( y  =  B  ->  ( A  u.  y )  =  ( A  u.  B ) )
86, 7eqeq12d 2486 . 2  |-  ( y  =  B  ->  ( U. { A ,  y }  =  ( A  u.  y )  <->  U. { A ,  B }  =  ( A  u.  B ) ) )
9 vex 3034 . . 3  |-  x  e. 
_V
10 vex 3034 . . 3  |-  y  e. 
_V
119, 10unipr 4203 . 2  |-  U. {
x ,  y }  =  ( x  u.  y )
124, 8, 11vtocl2g 3097 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  U. { A ,  B }  =  ( A  u.  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452    e. wcel 1904    u. cun 3388   {cpr 3961   U.cuni 4190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-v 3033  df-un 3395  df-sn 3960  df-pr 3962  df-uni 4191
This theorem is referenced by:  wunun  9153  tskun  9229  gruun  9249  mrcun  15606  unopn  20010  indistopon  20093  uncon  20521  limcun  22929  sshjval3  27088  prsiga  29027  unelsiga  29030  unelldsys  29054  measxun2  29106  measssd  29111  carsgsigalem  29220  carsgclctun  29226  pmeasmono  29230  probun  29325  indispcon  30029  kelac2  35994  fourierdlem70  38152  fourierdlem71  38153  saluncl  38290  prsal  38291  meadjun  38416  omeunle  38456
  Copyright terms: Public domain W3C validator