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

Theorem uniprg 4850
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 4667 . . . 4 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21unieqd 4846 . . 3 (𝑥 = 𝐴 {𝑥, 𝑦} = {𝐴, 𝑦})
3 uneq1 4135 . . 3 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
42, 3eqeq12d 2841 . 2 (𝑥 = 𝐴 → ( {𝑥, 𝑦} = (𝑥𝑦) ↔ {𝐴, 𝑦} = (𝐴𝑦)))
5 preq2 4668 . . . 4 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
65unieqd 4846 . . 3 (𝑦 = 𝐵 {𝐴, 𝑦} = {𝐴, 𝐵})
7 uneq2 4136 . . 3 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
86, 7eqeq12d 2841 . 2 (𝑦 = 𝐵 → ( {𝐴, 𝑦} = (𝐴𝑦) ↔ {𝐴, 𝐵} = (𝐴𝐵)))
9 vex 3502 . . 3 𝑥 ∈ V
10 vex 3502 . . 3 𝑦 ∈ V
119, 10unipr 4849 . 2 {𝑥, 𝑦} = (𝑥𝑦)
124, 8, 11vtocl2g 3576 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  cun 3937  {cpr 4565   cuni 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rex 3148  df-v 3501  df-un 3944  df-sn 4564  df-pr 4566  df-uni 4837
This theorem is referenced by:  unisng  4851  wunun  10124  tskun  10200  gruun  10220  mrcun  16885  unopn  21429  indistopon  21527  unconn  21955  limcun  24410  sshjval3  29047  prsiga  31278  unelsiga  31281  unelldsys  31305  measxun2  31357  measssd  31362  carsgsigalem  31461  carsgclctun  31467  pmeasmono  31470  probun  31565  indispconn  32367  kelac2  39532  mnuund  40481  fourierdlem70  42329  fourierdlem71  42330  saluncl  42470  prsal  42471  meadjun  42612  omeunle  42666
  Copyright terms: Public domain W3C validator