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

Theorem uniprg 4386
 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 4212 . . . 4 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21unieqd 4382 . . 3 (𝑥 = 𝐴 {𝑥, 𝑦} = {𝐴, 𝑦})
3 uneq1 3722 . . 3 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
42, 3eqeq12d 2625 . 2 (𝑥 = 𝐴 → ( {𝑥, 𝑦} = (𝑥𝑦) ↔ {𝐴, 𝑦} = (𝐴𝑦)))
5 preq2 4213 . . . 4 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
65unieqd 4382 . . 3 (𝑦 = 𝐵 {𝐴, 𝑦} = {𝐴, 𝐵})
7 uneq2 3723 . . 3 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
86, 7eqeq12d 2625 . 2 (𝑦 = 𝐵 → ( {𝐴, 𝑦} = (𝐴𝑦) ↔ {𝐴, 𝐵} = (𝐴𝐵)))
9 vex 3176 . . 3 𝑥 ∈ V
10 vex 3176 . . 3 𝑦 ∈ V
119, 10unipr 4385 . 2 {𝑥, 𝑦} = (𝑥𝑦)
124, 8, 11vtocl2g 3243 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∪ cun 3538  {cpr 4127  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128  df-uni 4373 This theorem is referenced by:  wunun  9411  tskun  9487  gruun  9507  mrcun  16105  unopn  20533  indistopon  20615  uncon  21042  limcun  23465  sshjval3  27597  prsiga  29521  unelsiga  29524  unelldsys  29548  measxun2  29600  measssd  29605  carsgsigalem  29704  carsgclctun  29710  pmeasmono  29713  probun  29808  indispcon  30470  kelac2  36653  fourierdlem70  39069  fourierdlem71  39070  saluncl  39213  prsal  39214  meadjun  39355  omeunle  39406
 Copyright terms: Public domain W3C validator