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

Theorem uniprg 4482
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 4300 . . . 4 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21unieqd 4478 . . 3 (𝑥 = 𝐴 {𝑥, 𝑦} = {𝐴, 𝑦})
3 uneq1 3793 . . 3 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
42, 3eqeq12d 2666 . 2 (𝑥 = 𝐴 → ( {𝑥, 𝑦} = (𝑥𝑦) ↔ {𝐴, 𝑦} = (𝐴𝑦)))
5 preq2 4301 . . . 4 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
65unieqd 4478 . . 3 (𝑦 = 𝐵 {𝐴, 𝑦} = {𝐴, 𝐵})
7 uneq2 3794 . . 3 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
86, 7eqeq12d 2666 . 2 (𝑦 = 𝐵 → ( {𝐴, 𝑦} = (𝐴𝑦) ↔ {𝐴, 𝐵} = (𝐴𝐵)))
9 vex 3234 . . 3 𝑥 ∈ V
10 vex 3234 . . 3 𝑦 ∈ V
119, 10unipr 4481 . 2 {𝑥, 𝑦} = (𝑥𝑦)
124, 8, 11vtocl2g 3301 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  cun 3605  {cpr 4212   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213  df-uni 4469
This theorem is referenced by:  wunun  9570  tskun  9646  gruun  9666  mrcun  16329  unopn  20756  indistopon  20853  unconn  21280  limcun  23704  sshjval3  28341  prsiga  30322  unelsiga  30325  unelldsys  30349  measxun2  30401  measssd  30406  carsgsigalem  30505  carsgclctun  30511  pmeasmono  30514  probun  30609  indispconn  31342  kelac2  37952  fourierdlem70  40711  fourierdlem71  40712  saluncl  40855  prsal  40856  meadjun  40997  omeunle  41051
  Copyright terms: Public domain W3C validator