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

Theorem uniprg 4672
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 4486 . . . 4 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21unieqd 4668 . . 3 (𝑥 = 𝐴 {𝑥, 𝑦} = {𝐴, 𝑦})
3 uneq1 3987 . . 3 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
42, 3eqeq12d 2840 . 2 (𝑥 = 𝐴 → ( {𝑥, 𝑦} = (𝑥𝑦) ↔ {𝐴, 𝑦} = (𝐴𝑦)))
5 preq2 4487 . . . 4 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
65unieqd 4668 . . 3 (𝑦 = 𝐵 {𝐴, 𝑦} = {𝐴, 𝐵})
7 uneq2 3988 . . 3 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
86, 7eqeq12d 2840 . 2 (𝑦 = 𝐵 → ( {𝐴, 𝑦} = (𝐴𝑦) ↔ {𝐴, 𝐵} = (𝐴𝐵)))
9 vex 3417 . . 3 𝑥 ∈ V
10 vex 3417 . . 3 𝑦 ∈ V
119, 10unipr 4671 . 2 {𝑥, 𝑦} = (𝑥𝑦)
124, 8, 11vtocl2g 3486 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wcel 2166  cun 3796  {cpr 4399   cuni 4658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-v 3416  df-un 3803  df-sn 4398  df-pr 4400  df-uni 4659
This theorem is referenced by:  unisng  4673  wunun  9847  tskun  9923  gruun  9943  mrcun  16635  unopn  21078  indistopon  21176  unconn  21603  limcun  24058  sshjval3  28768  prsiga  30739  unelsiga  30742  unelldsys  30766  measxun2  30818  measssd  30823  carsgsigalem  30922  carsgclctun  30928  pmeasmono  30931  probun  31027  indispconn  31762  kelac2  38478  fourierdlem70  41187  fourierdlem71  41188  saluncl  41328  prsal  41329  meadjun  41470  omeunle  41524
  Copyright terms: Public domain W3C validator