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

Theorem ssint 4964
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 3972 . 2 (𝐴 𝐵 ↔ ∀𝑦𝐴 𝑦 𝐵)
2 vex 3484 . . . 4 𝑦 ∈ V
32elint2 4953 . . 3 (𝑦 𝐵 ↔ ∀𝑥𝐵 𝑦𝑥)
43ralbii 3093 . 2 (∀𝑦𝐴 𝑦 𝐵 ↔ ∀𝑦𝐴𝑥𝐵 𝑦𝑥)
5 ralcom 3289 . . 3 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
6 dfss3 3972 . . . 4 (𝐴𝑥 ↔ ∀𝑦𝐴 𝑦𝑥)
76ralbii 3093 . . 3 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
85, 7bitr4i 278 . 2 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥)
91, 4, 83bitri 297 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2108  wral 3061  wss 3951   cint 4946
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-11 2157  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-int 4947
This theorem is referenced by:  ssintab  4965  ssintub  4966  iinpw  5106  oneqmini  6436  fint  6787  fnssintima  7382  sorpssint  7753  iscard2  10016  coftr  10313  isf32lem2  10394  inttsk  10814  dfrtrcl2  15101  isacs1i  17700  mrelatglb  18605  fbfinnfr  23849  fclscmp  24038  noextenddif  27713  eqscut2  27851  scutun12  27855  ssdifidllem  33484  ssmxidllem  33501  fneint  36349  topmeet  36365  igenval2  38073  ismrcd1  42709  onintunirab  43239  dftrcl3  43733  dfrtrcl3  43746  sssalgen  46350  issalgend  46353  intubeu  48873  ipoglblem  48878
  Copyright terms: Public domain W3C validator