Theorem uniprg 4263

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

Proof of Theorem uniprg

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq1 4109	. . . 4
2	1	unieqd 4259	. . 3
3		uneq1 3650	. . 3
4	2, 3	eqeq12d 2479	. 2
5		preq2 4110	. . . 4
6	5	unieqd 4259	. . 3
7		uneq2 3651	. . 3
8	6, 7	eqeq12d 2479	. 2
9		vex 3112	. . 3
10		vex 3112	. . 3
11	9, 10	unipr 4262	. 2
12	4, 8, 11	vtocl2g 3171	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  u.cun 3473  {cpr 4031  U.cuni 4249

This theorem is referenced by:  wunun  9109  tskun  9185  gruun  9205  mrcun  15019  unopn  19412  indistopon  19502  uncon  19930  limcun  22299  sshjval3  26272  prsiga  28131  unelsiga  28134  measxun2  28181  measssd  28186  probun  28358  indispcon  28679  kelac2  31011  fourierdlem70  31959  fourierdlem71  31960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250