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

Theorem uniprg 3842
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 3706 . . . 4  |-  ( x  =  A  ->  { x ,  y }  =  { A ,  y } )
21unieqd 3838 . . 3  |-  ( x  =  A  ->  U. {
x ,  y }  =  U. { A ,  y } )
3 uneq1 3322 . . 3  |-  ( x  =  A  ->  (
x  u.  y )  =  ( A  u.  y ) )
42, 3eqeq12d 2297 . 2  |-  ( x  =  A  ->  ( U. { x ,  y }  =  ( x  u.  y )  <->  U. { A ,  y }  =  ( A  u.  y
) ) )
5 preq2 3707 . . . 4  |-  ( y  =  B  ->  { A ,  y }  =  { A ,  B }
)
65unieqd 3838 . . 3  |-  ( y  =  B  ->  U. { A ,  y }  =  U. { A ,  B } )
7 uneq2 3323 . . 3  |-  ( y  =  B  ->  ( A  u.  y )  =  ( A  u.  B ) )
86, 7eqeq12d 2297 . 2  |-  ( y  =  B  ->  ( U. { A ,  y }  =  ( A  u.  y )  <->  U. { A ,  B }  =  ( A  u.  B ) ) )
9 vex 2791 . . 3  |-  x  e. 
_V
10 vex 2791 . . 3  |-  y  e. 
_V
119, 10unipr 3841 . 2  |-  U. {
x ,  y }  =  ( x  u.  y )
124, 8, 11vtocl2g 2847 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  U. { A ,  B }  =  ( A  u.  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684    u. cun 3150   {cpr 3641   U.cuni 3827
This theorem is referenced by:  wunun  8332  tskun  8408  gruun  8428  mrcun  13524  unopn  16649  indistopon  16738  uncon  17155  limcun  19245  sshjval3  21933  prsiga  23492  unelsiga  23495  measxun2  23538  measssd  23543  probun  23622  indispcon  23765  kelac2  27163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator