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

Theorem intss 4974
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 4051 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝑦𝑥 → ∀𝑥𝐴 𝑦𝑥))
21ss2abdv 4061 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4953 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4953 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 4028 1 (𝐴𝐵 𝐵 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2710  wral 3062  wss 3949   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-int 4952
This theorem is referenced by:  uniintsn  4992  intabs  5343  cofon1  8671  naddssim  8684  fiss  9419  tc2  9737  tcss  9739  tcel  9740  rankval4  9862  cfub  10244  cflm  10245  cflecard  10248  fin23lem26  10320  clsslem  14931  mrcss  17560  lspss  20595  lbsextlem3  20773  aspss  21431  clsss  22558  1stcfb  22949  ufinffr  23433  cofcut1  27407  spanss  30601  fldgenss  32406  ss2mcls  34559  pclssN  38765  dochspss  40249  clss2lem  42362
  Copyright terms: Public domain W3C validator