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

Theorem unissb 4621
Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
Assertion
Ref Expression
unissb ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem unissb
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eluni 4591 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 338 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 2020 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 267 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1896 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 alcom 2186 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
7 19.21v 2017 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
8 impexp 461 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
9 bi2.04 375 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
108, 9bitri 264 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1110albii 1896 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
12 dfss2 3732 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
1312imbi2i 325 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
147, 11, 133bitr4i 292 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
1514albii 1896 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
166, 15bitri 264 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
175, 16bitri 264 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
18 dfss2 3732 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
19 df-ral 3055 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2017, 18, 193bitr4i 292 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1630  wex 1853  wcel 2139  wral 3050  wss 3715   cuni 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-v 3342  df-in 3722  df-ss 3729  df-uni 4589
This theorem is referenced by:  uniss2  4622  ssunieq  4624  sspwuni  4763  pwssb  4764  ordunisssuc  5991  sorpssuni  7112  bm2.5ii  7172  sbthlem1  8237  ordunifi  8377  isfinite2  8385  cflim2  9297  fin23lem16  9369  fin23lem29  9375  fin1a2lem11  9444  fin1a2lem13  9446  itunitc  9455  zorng  9538  wuncval2  9781  suplem1pr  10086  suplem2pr  10087  mrcuni  16503  ipodrsfi  17384  mrelatlub  17407  subgint  17839  efgval  18350  toponmre  21119  neips  21139  neiuni  21148  alexsubALTlem2  22073  alexsubALTlem3  22074  tgpconncompeqg  22136  unidmvol  23529  tglnunirn  25663  uniinn0  29694  locfinreflem  30237  sxbrsigalem0  30663  dya2iocuni  30675  dya2iocucvr  30676  carsguni  30700  topjoin  32687  fnejoin1  32690  fnejoin2  32691  ovoliunnfl  33782  voliunnfl  33784  volsupnfl  33785  intidl  34159  unichnidl  34161  salexct  41073  setrec1lem2  42963  setrec2fun  42967
  Copyright terms: Public domain W3C validator