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

Theorem unissb 4939
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 2157. (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 4910 . . . . . 6 (𝑦 𝐴 ↔ ∃𝑥(𝑦𝑥𝑥𝐴))
21imbi1i 349 . . . . 5 ((𝑦 𝐴𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
3 19.23v 1942 . . . . 5 (∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (∃𝑥(𝑦𝑥𝑥𝐴) → 𝑦𝐵))
42, 3bitr4i 278 . . . 4 ((𝑦 𝐴𝑦𝐵) ↔ ∀𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
54albii 1819 . . 3 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
6 elequ1 2115 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
76anbi1d 631 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑧𝑥𝑥𝐴)))
8 eleq1w 2824 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
97, 8imbi12d 344 . . . . 5 (𝑦 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑧𝑥𝑥𝐴) → 𝑧𝐵)))
10 elequ2 2123 . . . . . . 7 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
11 eleq1w 2824 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1210, 11anbi12d 632 . . . . . 6 (𝑥 = 𝑧 → ((𝑦𝑥𝑥𝐴) ↔ (𝑦𝑧𝑧𝐴)))
1312imbi1d 341 . . . . 5 (𝑥 = 𝑧 → (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ((𝑦𝑧𝑧𝐴) → 𝑦𝐵)))
149, 13alcomw 2044 . . . 4 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵))
15 19.21v 1939 . . . . . 6 (∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
16 impexp 450 . . . . . . . 8 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑦𝑥 → (𝑥𝐴𝑦𝐵)))
17 bi2.04 387 . . . . . . . 8 ((𝑦𝑥 → (𝑥𝐴𝑦𝐵)) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1816, 17bitri 275 . . . . . . 7 (((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
1918albii 1819 . . . . . 6 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝑥𝑦𝐵)))
20 df-ss 3968 . . . . . . 7 (𝑥𝐵 ↔ ∀𝑦(𝑦𝑥𝑦𝐵))
2120imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝑥𝑦𝐵)))
2215, 19, 213bitr4i 303 . . . . 5 (∀𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ (𝑥𝐴𝑥𝐵))
2322albii 1819 . . . 4 (∀𝑥𝑦((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2414, 23bitri 275 . . 3 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
255, 24bitri 275 . 2 (∀𝑦(𝑦 𝐴𝑦𝐵) ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
26 df-ss 3968 . 2 ( 𝐴𝐵 ↔ ∀𝑦(𝑦 𝐴𝑦𝐵))
27 df-ral 3062 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2825, 26, 273bitr4i 303 1 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wex 1779  wcel 2108  wral 3061  wss 3951   cuni 4907
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908
This theorem is referenced by:  uniss2  4941  ssunieq  4943  sspwuni  5100  pwssb  5101  ordunisssuc  6490  sorpssuni  7752  uniordint  7821  sbthlem1  9123  ordunifi  9326  isfinite2  9334  cflim2  10303  fin23lem16  10375  fin23lem29  10381  fin1a2lem11  10450  fin1a2lem13  10452  itunitc  10461  zorng  10544  wuncval2  10787  suplem1pr  11092  suplem2pr  11093  mrcuni  17664  ipodrsfi  18584  mrelatlub  18607  subgint  19168  efgval  19735  toponmre  23101  neips  23121  neiuni  23130  alexsubALTlem2  24056  alexsubALTlem3  24057  tgpconncompeqg  24120  unidmvol  25576  oldf  27896  tglnunirn  28556  uniinn0  32563  elrspunidl  33456  ssdifidllem  33484  ssmxidllem  33501  locfinreflem  33839  zarclsiin  33870  zarclsint  33871  zarcmplem  33880  sxbrsigalem0  34273  dya2iocuni  34285  dya2iocucvr  34286  carsguni  34310  topjoin  36366  fnejoin1  36369  fnejoin2  36370  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  intidl  38036  unichnidl  38038  onuniintrab  43238  onsupmaxb  43251  onsupnub  43261  mnuunid  44296  expanduniss  44312  salexct  46349  unilbss  48737  unilbeu  48874  ipolublem  48875  setrec1lem2  49207  setrec2fun  49211
  Copyright terms: Public domain W3C validator