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

Theorem unissb 4943
Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) Avoid ax-11 2146. (Revised by BTernaryTau, 28-Dec-2024.)
Assertion
Ref Expression
unissb ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem unissb
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 4912 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 348 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1937 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 277 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1813 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 elequ1 2105 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
76anbi1d 629 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑧𝑥𝑥𝐴)))
8 eleq1w 2808 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
97, 8imbi12d 343 . . . . 5 (𝑦 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑧𝑥𝑥𝐴) → 𝑧𝐵)))
10 elequ2 2113 . . . . . . 7 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
11 eleq1w 2808 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1210, 11anbi12d 630 . . . . . 6 (𝑥 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑦𝑧𝑧𝐴)))
1312imbi1d 340 . . . . 5 (𝑥 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑦𝑧𝑧𝐴) → 𝑦𝐵)))
149, 13alcomw 2039 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
15 19.21v 1934 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
16 impexp 449 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
17 bi2.04 386 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1816, 17bitri 274 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1918albii 1813 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
20 df-ss 3961 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
2120imbi2i 335 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
2215, 19, 213bitr4i 302 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
2322albii 1813 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2414, 23bitri 274 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
255, 24bitri 274 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
26 df-ss 3961 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
27 df-ral 3051 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2825, 26, 273bitr4i 302 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531  wex 1773  wcel 2098  wral 3050  wss 3944   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-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3961  df-uni 4910
This theorem is referenced by:  uniss2  4945  ssunieq  4947  sspwuni  5104  pwssb  5105  ordunisssuc  6477  sorpssuni  7738  uniordint  7805  sbthlem1  9111  ordunifi  9321  isfinite2  9329  cflim2  10293  fin23lem16  10365  fin23lem29  10371  fin1a2lem11  10440  fin1a2lem13  10442  itunitc  10451  zorng  10534  wuncval2  10777  suplem1pr  11082  suplem2pr  11083  mrcuni  17609  ipodrsfi  18539  mrelatlub  18562  subgint  19118  efgval  19689  toponmre  23046  neips  23066  neiuni  23075  alexsubALTlem2  24001  alexsubALTlem3  24002  tgpconncompeqg  24065  unidmvol  25519  oldf  27835  tglnunirn  28429  uniinn0  32425  elrspunidl  33245  ssdifidllem  33273  ssmxidllem  33290  locfinreflem  33574  zarclsiin  33605  zarclsint  33606  zarcmplem  33615  sxbrsigalem0  34024  dya2iocuni  34036  dya2iocucvr  34037  carsguni  34061  topjoin  35982  fnejoin1  35985  fnejoin2  35986  ovoliunnfl  37268  voliunnfl  37270  volsupnfl  37271  intidl  37635  unichnidl  37637  onuniintrab  42798  onsupmaxb  42811  onsupnub  42821  mnuunid  43858  expanduniss  43874  salexct  45862  unilbss  48076  unilbeu  48184  ipolublem  48185  setrec1lem2  48307  setrec2fun  48311
  Copyright terms: Public domain W3C validator