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

Theorem ssin 4246
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 3978 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
21imbi2i 336 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
32albii 1815 . . 3 (∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ ∀𝑥(𝑥𝐴 → (𝑥𝐵𝑥𝐶)))
4 jcab 517 . . . 4 ((𝑥𝐴 → (𝑥𝐵𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)))
54albii 1815 . . 3 (∀𝑥(𝑥𝐴 → (𝑥𝐵𝑥𝐶)) ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)))
6 19.26 1867 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ∧ (𝑥𝐴𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)))
73, 5, 63bitrri 298 . 2 ((∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
8 df-ss 3979 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
9 df-ss 3979 . . 3 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
108, 9anbi12i 628 . 2 ((𝐴𝐵𝐴𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐴𝑥𝐶)))
11 df-ss 3979 . 2 (𝐴 ⊆ (𝐵𝐶) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐵𝐶)))
127, 10, 113bitr4i 303 1 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1534  wcel 2105  cin 3961  wss 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979
This theorem is referenced by:  ssini  4247  ssind  4248  uneqin  4294  disjpss  4466  trin  5276  pwin  5578  fin  6788  frrlem4  8312  frrlem13  8321  wfrlem4OLD  8350  epfrs  9768  tcmin  9778  resscntz  19363  subgdmdprd  20068  tgval  22977  eltg3i  22983  innei  23148  cnprest2  23313  subislly  23504  lly1stc  23519  xkohaus  23676  xkoinjcn  23710  opnfbas  23865  supfil  23918  rnelfm  23976  tsmsres  24167  restmetu  24598  chabs2  31545  cmbr4i  31629  pjin3i  32222  mdbr2  32324  dmdbr2  32331  dmdbr5  32336  mdslle1i  32345  mdslle2i  32346  mdslj1i  32347  mdslj2i  32348  mdsl2i  32350  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd1i  32357  mdslmd3i  32360  hatomistici  32390  chrelat2i  32393  cvexchlem  32396  mdsymlem1  32431  mdsymlem3  32433  mdsymlem6  32436  dmdbr5ati  32450  pnfneige0  33911  ballotlem2  34469  iccllysconn  35234  heibor1lem  37795  relssinxpdmrn  38330  dochexmidlem1  41442  superficl  43556  k0004lem1  44136  ismnushort  44296
  Copyright terms: Public domain W3C validator