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 4912 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 350 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1946 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 278 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1822 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 elequ1 2114 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
76anbi1d 631 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑧𝑥𝑥𝐴)))
8 eleq1w 2817 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
97, 8imbi12d 345 . . . . 5 (𝑦 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑧𝑥𝑥𝐴) → 𝑧𝐵)))
10 elequ2 2122 . . . . . . 7 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
11 eleq1w 2817 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1210, 11anbi12d 632 . . . . . 6 (𝑥 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑦𝑧𝑧𝐴)))
1312imbi1d 342 . . . . 5 (𝑥 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑦𝑧𝑧𝐴) → 𝑦𝐵)))
149, 13alcomw 2048 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
15 19.21v 1943 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
16 impexp 452 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
17 bi2.04 389 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1816, 17bitri 275 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1918albii 1822 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
20 dfss2 3969 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
2120imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
2215, 19, 213bitr4i 303 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
2322albii 1822 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2414, 23bitri 275 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
255, 24bitri 275 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
26 dfss2 3969 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
27 df-ral 3063 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2825, 26, 273bitr4i 303 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wex 1782  wcel 2107  wral 3062  wss 3949   cuni 4909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  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  7722  uniordint  7789  sbthlem1  9083  ordunifi  9293  isfinite2  9301  cflim2  10258  fin23lem16  10330  fin23lem29  10336  fin1a2lem11  10405  fin1a2lem13  10407  itunitc  10416  zorng  10499  wuncval2  10742  suplem1pr  11047  suplem2pr  11048  mrcuni  17565  ipodrsfi  18492  mrelatlub  18515  subgint  19030  efgval  19585  toponmre  22597  neips  22617  neiuni  22626  alexsubALTlem2  23552  alexsubALTlem3  23553  tgpconncompeqg  23616  unidmvol  25058  oldf  27352  tglnunirn  27799  uniinn0  31782  elrspunidl  32546  ssmxidllem  32589  locfinreflem  32820  zarclsiin  32851  zarclsint  32852  zarcmplem  32861  sxbrsigalem0  33270  dya2iocuni  33282  dya2iocucvr  33283  carsguni  33307  topjoin  35250  fnejoin1  35253  fnejoin2  35254  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  intidl  36897  unichnidl  36899  onuniintrab  41975  onsupmaxb  41988  onsupnub  41998  mnuunid  43036  expanduniss  43052  salexct  45050  unilbss  47502  unilbeu  47610  ipolublem  47611  setrec1lem2  47733  setrec2fun  47737
  Copyright terms: Public domain W3C validator