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 2152. (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 1943 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 277 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1819 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 elequ1 2111 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
76anbi1d 628 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑧𝑥𝑥𝐴)))
8 eleq1w 2814 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
97, 8imbi12d 343 . . . . 5 (𝑦 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑧𝑥𝑥𝐴) → 𝑧𝐵)))
10 elequ2 2119 . . . . . . 7 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
11 eleq1w 2814 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1210, 11anbi12d 629 . . . . . 6 (𝑥 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑦𝑧𝑧𝐴)))
1312imbi1d 340 . . . . 5 (𝑥 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑦𝑧𝑧𝐴) → 𝑦𝐵)))
149, 13alcomw 2045 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
15 19.21v 1940 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
16 impexp 449 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
17 bi2.04 386 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1816, 17bitri 274 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1918albii 1819 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
20 dfss2 3969 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
2120imbi2i 335 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
2215, 19, 213bitr4i 302 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
2322albii 1819 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2414, 23bitri 274 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
255, 24bitri 274 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
26 dfss2 3969 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
27 df-ral 3060 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2825, 26, 273bitr4i 302 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1537  wex 1779  wcel 2104  wral 3059  wss 3949   cuni 4909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-v 3474  df-in 3956  df-ss 3966  df-uni 4910
This theorem is referenced by:  uniss2  4946  ssunieq  4948  sspwuni  5104  pwssb  5105  ordunisssuc  6471  sorpssuni  7726  uniordint  7793  sbthlem1  9087  ordunifi  9297  isfinite2  9305  cflim2  10262  fin23lem16  10334  fin23lem29  10340  fin1a2lem11  10409  fin1a2lem13  10411  itunitc  10420  zorng  10503  wuncval2  10746  suplem1pr  11051  suplem2pr  11052  mrcuni  17571  ipodrsfi  18498  mrelatlub  18521  subgint  19068  efgval  19628  toponmre  22819  neips  22839  neiuni  22848  alexsubALTlem2  23774  alexsubALTlem3  23775  tgpconncompeqg  23838  unidmvol  25292  oldf  27587  tglnunirn  28064  uniinn0  32047  elrspunidl  32818  ssmxidllem  32861  locfinreflem  33116  zarclsiin  33147  zarclsint  33148  zarcmplem  33157  sxbrsigalem0  33566  dya2iocuni  33578  dya2iocucvr  33579  carsguni  33603  topjoin  35555  fnejoin1  35558  fnejoin2  35559  ovoliunnfl  36835  voliunnfl  36837  volsupnfl  36838  intidl  37202  unichnidl  37204  onuniintrab  42279  onsupmaxb  42292  onsupnub  42302  mnuunid  43340  expanduniss  43356  salexct  45350  unilbss  47591  unilbeu  47699  ipolublem  47700  setrec1lem2  47822  setrec2fun  47826
  Copyright terms: Public domain W3C validator