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

Theorem ssint 4969
Description: Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
ssint (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssint
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfss3 3984 . 2 (𝐴 𝐵 ↔ ∀𝑦𝐴 𝑦 𝐵)
2 vex 3482 . . . 4 𝑦 ∈ V
32elint2 4958 . . 3 (𝑦 𝐵 ↔ ∀𝑥𝐵 𝑦𝑥)
43ralbii 3091 . 2 (∀𝑦𝐴 𝑦 𝐵 ↔ ∀𝑦𝐴𝑥𝐵 𝑦𝑥)
5 ralcom 3287 . . 3 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
6 dfss3 3984 . . . 4 (𝐴𝑥 ↔ ∀𝑦𝐴 𝑦𝑥)
76ralbii 3091 . . 3 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
85, 7bitr4i 278 . 2 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥)
91, 4, 83bitri 297 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2106  wral 3059  wss 3963   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-ss 3980  df-int 4952
This theorem is referenced by:  ssintab  4970  ssintub  4971  iinpw  5111  oneqmini  6438  fint  6788  fnssintima  7382  sorpssint  7752  iscard2  10014  coftr  10311  isf32lem2  10392  inttsk  10812  dfrtrcl2  15098  isacs1i  17702  mrelatglb  18618  fbfinnfr  23865  fclscmp  24054  noextenddif  27728  eqscut2  27866  scutun12  27870  ssdifidllem  33464  ssmxidllem  33481  fneint  36331  topmeet  36347  igenval2  38053  ismrcd1  42686  onintunirab  43216  dftrcl3  43710  dfrtrcl3  43723  sssalgen  46291  issalgend  46294  intubeu  48773  ipoglblem  48778
  Copyright terms: Public domain W3C validator