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

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.
StepHypRef Expression
1 preq1 4109 . . . 4
21unieqd 4259 . . 3
3 uneq1 3650 . . 3
42, 3eqeq12d 2479 . 2
5 preq2 4110 . . . 4
65unieqd 4259 . . 3
7 uneq2 3651 . . 3
86, 7eqeq12d 2479 . 2
9 vex 3112 . . 3
10 vex 3112 . . 3
119, 10unipr 4262 . 2
124, 8, 11vtocl2g 3171 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator