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.

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

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