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.

Step	Hyp	Ref	Expression
1		preq1 4042	. . . 4 |- ( x = A -> { x , y } = { A , y } )
2	1	unieqd 4200	. . 3 |- ( x = A -> U. { x , y } = U. { A , y } )
3		uneq1 3572	. . 3 |- ( x = A -> ( x u. y ) = ( A u. y ) )
4	2, 3	eqeq12d 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 } )
6	5	unieqd 4200	. . 3 |- ( y = B -> U. { A , y } = U. { A , B } )
7		uneq2 3573	. . 3 |- ( y = B -> ( A u. y ) = ( A u. B ) )
8	6, 7	eqeq12d 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
11	9, 10	unipr 4203	. 2 |- U. { x , y } = ( x u. y )
12	4, 8, 11	vtocl2g 3097	1 |- ( ( A e. V /\ B e. W ) -> U. { A , B } = ( A u. B ) )

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