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

Theorem uniprg 4922
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 4923 to prove it from uniprg 4922. (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 3483 . . . . . . . . 9 𝑦 ∈ V
21elpr 4649 . . . . . . . 8 (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴𝑦 = 𝐵))
32anbi2i 623 . . . . . . 7 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)))
4 ancom 460 . . . . . . . 8 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦))
5 andir 1010 . . . . . . . 8 (((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
64, 5bitri 275 . . . . . . 7 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
73, 6bitri 275 . . . . . 6 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
87exbii 1847 . . . . 5 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
9 19.43 1881 . . . . 5 (∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
108, 9bitri 275 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
11 clel3g 3660 . . . . . . 7 (𝐴𝑉 → (𝑥𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑥𝑦)))
1211bicomd 223 . . . . . 6 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
1312adantr 480 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
14 clel3g 3660 . . . . . . 7 (𝐵𝑊 → (𝑥𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
1514bicomd 223 . . . . . 6 (𝐵𝑊 → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1615adantl 481 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1713, 16orbi12d 918 . . . 4 ((𝐴𝑉𝐵𝑊) → ((∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)) ↔ (𝑥𝐴𝑥𝐵)))
1810, 17bitrid 283 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝐴𝑥𝐵)))
1918abbidv 2807 . 2 ((𝐴𝑉𝐵𝑊) → {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
20 df-uni 4907 . 2 {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})}
21 df-un 3955 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2219, 20, 213eqtr4g 2801 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1539  wex 1778  wcel 2107  {cab 2713  cun 3948  {cpr 4627   cuni 4906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-sn 4626  df-pr 4628  df-uni 4907
This theorem is referenced by:  unipr  4923  unisng  4924  unexg  7764  wunun  10751  tskun  10827  gruun  10847  mrcun  17666  unopn  22910  indistopon  23009  unconn  23438  limcun  25931  sshjval3  31374  prsiga  34133  unelsiga  34136  unelldsys  34160  measxun2  34212  measssd  34217  carsgsigalem  34318  carsgclctun  34324  pmeasmono  34327  probun  34422  indispconn  35240  bj-prmoore  37117  kelac2  43082  onsucunipr  43390  onsucunitp  43391  oaun2  43399  oaun3  43400  mnuund  44302  fourierdlem70  46196  fourierdlem71  46197  saluncl  46337  prsal  46338  meadjun  46482  omeunle  46536  toplatjoin  48906
  Copyright terms: Public domain W3C validator