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

Theorem uniprg 4925
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 4926 to prove it from uniprg 4925. (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 3465 . . . . . . . . 9 𝑦 ∈ V
21elpr 4654 . . . . . . . 8 (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴𝑦 = 𝐵))
32anbi2i 621 . . . . . . 7 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)))
4 ancom 459 . . . . . . . 8 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦))
5 andir 1006 . . . . . . . 8 (((𝑦 = 𝐴𝑦 = 𝐵) ∧ 𝑥𝑦) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
64, 5bitri 274 . . . . . . 7 ((𝑥𝑦 ∧ (𝑦 = 𝐴𝑦 = 𝐵)) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
73, 6bitri 274 . . . . . 6 ((𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
87exbii 1842 . . . . 5 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ ∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)))
9 19.43 1877 . . . . 5 (∃𝑦((𝑦 = 𝐴𝑥𝑦) ∨ (𝑦 = 𝐵𝑥𝑦)) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
108, 9bitri 274 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
11 clel3g 3645 . . . . . . 7 (𝐴𝑉 → (𝑥𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑥𝑦)))
1211bicomd 222 . . . . . 6 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
1312adantr 479 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐴𝑥𝑦) ↔ 𝑥𝐴))
14 clel3g 3645 . . . . . . 7 (𝐵𝑊 → (𝑥𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑥𝑦)))
1514bicomd 222 . . . . . 6 (𝐵𝑊 → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1615adantl 480 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑦 = 𝐵𝑥𝑦) ↔ 𝑥𝐵))
1713, 16orbi12d 916 . . . 4 ((𝐴𝑉𝐵𝑊) → ((∃𝑦(𝑦 = 𝐴𝑥𝑦) ∨ ∃𝑦(𝑦 = 𝐵𝑥𝑦)) ↔ (𝑥𝐴𝑥𝐵)))
1810, 17bitrid 282 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵}) ↔ (𝑥𝐴𝑥𝐵)))
1918abbidv 2794 . 2 ((𝐴𝑉𝐵𝑊) → {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})} = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
20 df-uni 4910 . 2 {𝐴, 𝐵} = {𝑥 ∣ ∃𝑦(𝑥𝑦𝑦 ∈ {𝐴, 𝐵})}
21 df-un 3949 . 2 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
2219, 20, 213eqtr4g 2790 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wex 1773  wcel 2098  {cab 2702  cun 3942  {cpr 4632   cuni 4909
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-sn 4631  df-pr 4633  df-uni 4910
This theorem is referenced by:  unipr  4926  unisng  4929  wunun  10735  tskun  10811  gruun  10831  mrcun  17605  unopn  22849  indistopon  22948  unconn  23377  limcun  25868  sshjval3  31236  prsiga  33878  unelsiga  33881  unelldsys  33905  measxun2  33957  measssd  33962  carsgsigalem  34063  carsgclctun  34069  pmeasmono  34072  probun  34167  indispconn  34972  bj-prmoore  36722  kelac2  42628  onsucunipr  42940  onsucunitp  42941  oaun2  42949  oaun3  42950  mnuund  43854  fourierdlem70  45699  fourierdlem71  45700  saluncl  45840  prsal  45841  meadjun  45985  omeunle  46039  toplatjoin  48196
  Copyright terms: Public domain W3C validator