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

Theorem intss 4933
Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.)
Assertion
Ref Expression
intss (𝐴𝐵 𝐵 𝐴)

Proof of Theorem intss
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssralv 4005 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝑦𝑥 → ∀𝑥𝐴 𝑦𝑥))
21ss2abdv 4018 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4913 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4913 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 3989 1 (𝐴𝐵 𝐵 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2739  wral 3077  wss 3904   cint 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733
This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-ral 3078  df-ss 3921  df-int 4912
This theorem is referenced by:  uniintsn  4949  intabs  5319  cofon1  8657  naddssim  8671  fiss  9383  tc2  9708  tcss  9710  tcel  9711  rankval4  9838  cfub  10231  cflm  10232  cflecard  10235  fin23lem26  10308  clsslem  15021  mrcss  17671  lspss  21084  lbsextlem3  21263  aspss  22005  clsss  23190  1stcfb  23581  ufinffr  24065  cofcut1  28089  spanss  31666  fldgenss  33603  rankval4b  35459  ss2mcls  36026  pclssN  40636  dochspss  42120  clss2lem  44307
  Copyright terms: Public domain W3C validator