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

Theorem ssin 4239
Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
ssin ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))

Proof of Theorem ssin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3967 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
21imbi2i 336 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
32albii 1819 . . 3 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
4 jcab 517 . . . 4 ((𝑥𝐴 → (𝑥𝐵𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)))
54albii 1819 . . 3 (∀𝑥(𝑥𝐴 → (𝑥𝐵𝑥𝐶)) ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)))
6 19.26 1870 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)))
73, 5, 63bitrri 298 . 2 ((∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
8 df-ss 3968 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
9 df-ss 3968 . . 3 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
108, 9anbi12i 628 . 2 ((𝐴𝐵𝐴𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)))
11 df-ss 3968 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
127, 10, 113bitr4i 303 1 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wcel 2108  cin 3950  wss 3951
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-v 3482  df-in 3958  df-ss 3968
This theorem is referenced by:  ssini  4240  ssind  4241  uneqin  4289  disjpss  4461  trin  5271  pwin  5574  fin  6788  frrlem4  8314  frrlem13  8323  wfrlem4OLD  8352  epfrs  9771  tcmin  9781  resscntz  19351  subgdmdprd  20054  tgval  22962  eltg3i  22968  innei  23133  cnprest2  23298  subislly  23489  lly1stc  23504  xkohaus  23661  xkoinjcn  23695  opnfbas  23850  supfil  23903  rnelfm  23961  tsmsres  24152  restmetu  24583  chabs2  31536  cmbr4i  31620  pjin3i  32213  mdbr2  32315  dmdbr2  32322  dmdbr5  32327  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mdsl2i  32341  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd1i  32348  mdslmd3i  32351  hatomistici  32381  chrelat2i  32384  cvexchlem  32387  mdsymlem1  32422  mdsymlem3  32424  mdsymlem6  32427  dmdbr5ati  32441  pnfneige0  33950  ballotlem2  34491  iccllysconn  35255  heibor1lem  37816  relssinxpdmrn  38350  dochexmidlem1  41462  superficl  43580  k0004lem1  44160  ismnushort  44320
  Copyright terms: Public domain W3C validator