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

Theorem unissb 4405
 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 4375 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 338 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1889 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 266 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1737 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 alcom 2024 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
7 19.21v 1855 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
8 impexp 461 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
9 bi2.04 375 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
108, 9bitri 263 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1110albii 1737 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
12 dfss2 3557 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
1312imbi2i 325 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
147, 11, 133bitr4i 291 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
1514albii 1737 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
166, 15bitri 263 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
175, 16bitri 263 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
18 dfss2 3557 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
19 df-ral 2901 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2017, 18, 193bitr4i 291 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373 This theorem is referenced by:  uniss2  4406  ssunieq  4408  sspwuni  4547  pwssb  4548  ordunisssuc  5747  sorpssuni  6844  bm2.5ii  6898  sbthlem1  7955  ordunifi  8095  isfinite2  8103  cflim2  8968  fin23lem16  9040  fin23lem29  9046  fin1a2lem11  9115  fin1a2lem13  9117  itunitc  9126  zorng  9209  wuncval2  9448  suplem1pr  9753  suplem2pr  9754  mrcuni  16104  ipodrsfi  16986  mrelatlub  17009  subgint  17441  efgval  17953  toponmre  20707  neips  20727  neiuni  20736  alexsubALTlem2  21662  alexsubALTlem3  21663  tgpconcompeqg  21725  unidmvol  23116  tglnunirn  25243  uniinn0  28749  locfinreflem  29235  sxbrsigalem0  29660  dya2iocuni  29672  dya2iocucvr  29673  carsguni  29697  topjoin  31530  fnejoin1  31533  fnejoin2  31534  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  intidl  32998  unichnidl  33000  salexct  39228  setrec1lem2  42234  setrec2fun  42238
 Copyright terms: Public domain W3C validator