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

Theorem uniprg 4818
 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 4629 . . . 4 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21unieqd 4814 . . 3 (𝑥 = 𝐴 {𝑥, 𝑦} = {𝐴, 𝑦})
3 uneq1 4083 . . 3 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
42, 3eqeq12d 2814 . 2 (𝑥 = 𝐴 → ( {𝑥, 𝑦} = (𝑥𝑦) ↔ {𝐴, 𝑦} = (𝐴𝑦)))
5 preq2 4630 . . . 4 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
65unieqd 4814 . . 3 (𝑦 = 𝐵 {𝐴, 𝑦} = {𝐴, 𝐵})
7 uneq2 4084 . . 3 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
86, 7eqeq12d 2814 . 2 (𝑦 = 𝐵 → ( {𝐴, 𝑦} = (𝐴𝑦) ↔ {𝐴, 𝐵} = (𝐴𝐵)))
9 vex 3444 . . 3 𝑥 ∈ V
10 vex 3444 . . 3 𝑦 ∈ V
119, 10unipr 4817 . 2 {𝑥, 𝑦} = (𝑥𝑦)
124, 8, 11vtocl2g 3520 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∪ cun 3879  {cpr 4527  ∪ cuni 4800 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-uni 4801 This theorem is referenced by:  unisng  4819  wunun  10123  tskun  10199  gruun  10219  mrcun  16887  unopn  21515  indistopon  21613  unconn  22041  limcun  24505  sshjval3  29144  prsiga  31512  unelsiga  31515  unelldsys  31539  measxun2  31591  measssd  31596  carsgsigalem  31695  carsgclctun  31701  pmeasmono  31704  probun  31799  indispconn  32606  bj-prmoore  34546  kelac2  40024  mnuund  41001  fourierdlem70  42833  fourierdlem71  42834  saluncl  42974  prsal  42975  meadjun  43116  omeunle  43170
 Copyright terms: Public domain W3C validator