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

Theorem ssint 4962
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 3967 . 2 (𝐴 𝐵 ↔ ∀𝑦𝐴 𝑦 𝐵)
2 vex 3478 . . . 4 𝑦 ∈ V
32elint2 4951 . . 3 (𝑦 𝐵 ↔ ∀𝑥𝐵 𝑦𝑥)
43ralbii 3093 . 2 (∀𝑦𝐴 𝑦 𝐵 ↔ ∀𝑦𝐴𝑥𝐵 𝑦𝑥)
5 ralcom 3286 . . 3 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
6 dfss3 3967 . . . 4 (𝐴𝑥 ↔ ∀𝑦𝐴 𝑦𝑥)
76ralbii 3093 . . 3 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
85, 7bitr4i 277 . 2 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥)
91, 4, 83bitri 296 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2106  wral 3061  wss 3945   cint 4944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3952  df-ss 3962  df-int 4945
This theorem is referenced by:  ssintab  4963  ssintub  4964  iinpw  5103  oneqmini  6406  fint  6758  fnssintima  7344  sorpssint  7707  iscard2  9955  coftr  10252  isf32lem2  10333  inttsk  10753  dfrtrcl2  14993  isacs1i  17585  mrelatglb  18497  fbfinnfr  23276  fclscmp  23465  noextenddif  27100  eqscut2  27236  scutun12  27240  ssmxidllem  32502  fneint  35101  topmeet  35117  igenval2  36803  ismrcd1  41271  onintunirab  41811  dftrcl3  42306  dfrtrcl3  42319  sssalgen  44888  issalgend  44891  intubeu  47321  ipoglblem  47326
  Copyright terms: Public domain W3C validator