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

Theorem unissb 4944
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 2155. (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 4915 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 349 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1940 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 278 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1816 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 elequ1 2113 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
76anbi1d 631 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑧𝑥𝑥𝐴)))
8 eleq1w 2822 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
97, 8imbi12d 344 . . . . 5 (𝑦 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑧𝑥𝑥𝐴) → 𝑧𝐵)))
10 elequ2 2121 . . . . . . 7 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
11 eleq1w 2822 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1210, 11anbi12d 632 . . . . . 6 (𝑥 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑦𝑧𝑧𝐴)))
1312imbi1d 341 . . . . 5 (𝑥 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑦𝑧𝑧𝐴) → 𝑦𝐵)))
149, 13alcomw 2042 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
15 19.21v 1937 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
16 impexp 450 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
17 bi2.04 387 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1816, 17bitri 275 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1918albii 1816 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
20 df-ss 3980 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
2120imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
2215, 19, 213bitr4i 303 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
2322albii 1816 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2414, 23bitri 275 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
255, 24bitri 275 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
26 df-ss 3980 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
27 df-ral 3060 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2825, 26, 273bitr4i 303 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  wex 1776  wcel 2106  wral 3059  wss 3963   cuni 4912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-ss 3980  df-uni 4913
This theorem is referenced by:  uniss2  4946  ssunieq  4948  sspwuni  5105  pwssb  5106  ordunisssuc  6492  sorpssuni  7751  uniordint  7821  sbthlem1  9122  ordunifi  9324  isfinite2  9332  cflim2  10301  fin23lem16  10373  fin23lem29  10379  fin1a2lem11  10448  fin1a2lem13  10450  itunitc  10459  zorng  10542  wuncval2  10785  suplem1pr  11090  suplem2pr  11091  mrcuni  17666  ipodrsfi  18597  mrelatlub  18620  subgint  19181  efgval  19750  toponmre  23117  neips  23137  neiuni  23146  alexsubALTlem2  24072  alexsubALTlem3  24073  tgpconncompeqg  24136  unidmvol  25590  oldf  27911  tglnunirn  28571  uniinn0  32571  elrspunidl  33436  ssdifidllem  33464  ssmxidllem  33481  locfinreflem  33801  zarclsiin  33832  zarclsint  33833  zarcmplem  33842  sxbrsigalem0  34253  dya2iocuni  34265  dya2iocucvr  34266  carsguni  34290  topjoin  36348  fnejoin1  36351  fnejoin2  36352  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  intidl  38016  unichnidl  38018  onuniintrab  43215  onsupmaxb  43228  onsupnub  43238  mnuunid  44273  expanduniss  44289  salexct  46290  unilbss  48666  unilbeu  48774  ipolublem  48775  setrec1lem2  48919  setrec2fun  48923
  Copyright terms: Public domain W3C validator