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

Theorem unissb 4501
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 4471 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 338 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1911 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 267 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1787 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 alcom 2077 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
7 19.21v 1908 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
8 impexp 461 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
9 bi2.04 375 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
108, 9bitri 264 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1110albii 1787 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
12 dfss2 3624 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
1312imbi2i 325 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
147, 11, 133bitr4i 292 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
1514albii 1787 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
166, 15bitri 264 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
175, 16bitri 264 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
18 dfss2 3624 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
19 df-ral 2946 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2017, 18, 193bitr4i 292 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521  wex 1744  wcel 2030  wral 2941  wss 3607   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-in 3614  df-ss 3621  df-uni 4469
This theorem is referenced by:  uniss2  4502  ssunieq  4504  sspwuni  4643  pwssb  4644  ordunisssuc  5868  sorpssuni  6988  bm2.5ii  7048  sbthlem1  8111  ordunifi  8251  isfinite2  8259  cflim2  9123  fin23lem16  9195  fin23lem29  9201  fin1a2lem11  9270  fin1a2lem13  9272  itunitc  9281  zorng  9364  wuncval2  9607  suplem1pr  9912  suplem2pr  9913  mrcuni  16328  ipodrsfi  17210  mrelatlub  17233  subgint  17665  efgval  18176  toponmre  20945  neips  20965  neiuni  20974  alexsubALTlem2  21899  alexsubALTlem3  21900  tgpconncompeqg  21962  unidmvol  23355  tglnunirn  25488  uniinn0  29492  locfinreflem  30035  sxbrsigalem0  30461  dya2iocuni  30473  dya2iocucvr  30474  carsguni  30498  topjoin  32485  fnejoin1  32488  fnejoin2  32489  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  intidl  33958  unichnidl  33960  salexct  40870  setrec1lem2  42760  setrec2fun  42764
  Copyright terms: Public domain W3C validator