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

Theorem uniprg 4924
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.) Avoid using unipr 4925 to prove it from uniprg 4924. (Revised by BJ, 1-Sep-2024.)
Assertion
Ref Expression
uniprg ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))

Proof of Theorem uniprg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3479 . . . . . . . . 9 𝑦 ∈ V
21elpr 4650 . . . . . . . 8 (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴𝑦 = 𝐵))
32anbi2i 624 . . . . . . 7 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)))
4 ancom 462 . . . . . . . 8 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦))
5 andir 1008 . . . . . . . 8 (((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
64, 5bitri 275 . . . . . . 7 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
73, 6bitri 275 . . . . . 6 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
87exbii 1851 . . . . 5 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
9 19.43 1886 . . . . 5 (∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
108, 9bitri 275 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
11 clel3g 3649 . . . . . . 7 (𝐴𝑉 → (𝑥𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑥𝑦)))
1211bicomd 222 . . . . . 6 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
1312adantr 482 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
14 clel3g 3649 . . . . . . 7 (𝐵𝑊 → (𝑥𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
1514bicomd 222 . . . . . 6 (𝐵𝑊 → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1615adantl 483 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1713, 16orbi12d 918 . . . 4 ((𝐴𝑉𝐵𝑊) → ((∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)) ↔ (𝑥𝐴𝑥𝐵)))
1810, 17bitrid 283 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝐴𝑥𝐵)))
1918abbidv 2802 . 2 ((𝐴𝑉𝐵𝑊) → {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
20 df-uni 4908 . 2 {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})}
21 df-un 3952 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2219, 20, 213eqtr4g 2798 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wex 1782  wcel 2107  {cab 2710  cun 3945  {cpr 4629   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-sn 4628  df-pr 4630  df-uni 4908
This theorem is referenced by:  unipr  4925  unisng  4928  wunun  10701  tskun  10777  gruun  10797  mrcun  17562  unopn  22387  indistopon  22486  unconn  22915  limcun  25394  sshjval3  30585  prsiga  33067  unelsiga  33070  unelldsys  33094  measxun2  33146  measssd  33151  carsgsigalem  33252  carsgclctun  33258  pmeasmono  33261  probun  33356  indispconn  34163  bj-prmoore  35934  kelac2  41740  onsucunipr  42055  onsucunitp  42056  oaun2  42064  oaun3  42065  mnuund  42970  fourierdlem70  44827  fourierdlem71  44828  saluncl  44968  prsal  44969  meadjun  45113  omeunle  45167  toplatjoin  47529
  Copyright terms: Public domain W3C validator