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

Theorem ssint 4798
 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 3878 . 2 (𝐴 𝐵 ↔ ∀𝑦𝐴 𝑦 𝐵)
2 vex 3440 . . . 4 𝑦 ∈ V
32elint2 4789 . . 3 (𝑦 𝐵 ↔ ∀𝑥𝐵 𝑦𝑥)
43ralbii 3132 . 2 (∀𝑦𝐴 𝑦 𝐵 ↔ ∀𝑦𝐴𝑥𝐵 𝑦𝑥)
5 ralcom 3315 . . 3 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
6 dfss3 3878 . . . 4 (𝐴𝑥 ↔ ∀𝑦𝐴 𝑦𝑥)
76ralbii 3132 . . 3 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
85, 7bitr4i 279 . 2 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥)
91, 4, 83bitri 298 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∈ wcel 2081  ∀wral 3105   ⊆ wss 3859  ∩ cint 4782 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439  df-in 3866  df-ss 3874  df-int 4783 This theorem is referenced by:  ssintab  4799  ssintub  4800  iinpw  4927  oneqmini  6117  fint  6426  sorpssint  7317  iscard2  9251  coftr  9541  isf32lem2  9622  inttsk  10042  dfrtrcl2  14255  isacs1i  16757  mrelatglb  17623  fbfinnfr  22133  fclscmp  22322  noextenddif  32784  scutun12  32880  fneint  33305  topmeet  33321  igenval2  34876  ismrcd1  38780  dftrcl3  39550  dfrtrcl3  39563  sssalgen  42160  issalgend  42163
 Copyright terms: Public domain W3C validator