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.

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

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