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

Theorem ssint 4419
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 3554 . 2 (𝐴 𝐵 ↔ ∀𝑦𝐴 𝑦 𝐵)
2 vex 3172 . . . 4 𝑦 ∈ V
32elint2 4408 . . 3 (𝑦 𝐵 ↔ ∀𝑥𝐵 𝑦𝑥)
43ralbii 2959 . 2 (∀𝑦𝐴 𝑦 𝐵 ↔ ∀𝑦𝐴𝑥𝐵 𝑦𝑥)
5 ralcom 3075 . . 3 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
6 dfss3 3554 . . . 4 (𝐴𝑥 ↔ ∀𝑦𝐴 𝑦𝑥)
76ralbii 2959 . . 3 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥𝐵𝑦𝐴 𝑦𝑥)
85, 7bitr4i 265 . 2 (∀𝑦𝐴𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥)
91, 4, 83bitri 284 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1976  wral 2892  wss 3536   cint 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-v 3171  df-in 3543  df-ss 3550  df-int 4402
This theorem is referenced by:  ssintab  4420  ssintub  4421  iinpw  4541  trint  4687  oneqmini  5676  fint  5979  sorpssint  6819  iscard2  8659  coftr  8952  isf32lem2  9033  inttsk  9449  dfrtrcl2  13593  isacs1i  16084  mrelatglb  16950  fbfinnfr  21394  fclscmp  21583  fneint  31316  topmeet  31332  igenval2  32835  ismrcd1  36079  dftrcl3  36831  dfrtrcl3  36844  sssalgen  39030  issalgend  39033
  Copyright terms: Public domain W3C validator