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 4064 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝑦𝑥 → ∀𝑥𝐴 𝑦𝑥))
21ss2abdv 4076 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4953 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4953 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 4041 1 (𝐴𝐵 𝐵 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2712  wral 3059  wss 3963   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ral 3060  df-ss 3980  df-int 4952
This theorem is referenced by:  uniintsn  4990  intabs  5355  cofon1  8709  naddssim  8722  fiss  9462  tc2  9780  tcss  9782  tcel  9783  rankval4  9905  cfub  10287  cflm  10288  cflecard  10291  fin23lem26  10363  clsslem  15020  mrcss  17661  lspss  21000  lbsextlem3  21180  aspss  21915  clsss  23078  1stcfb  23469  ufinffr  23953  cofcut1  27969  spanss  31377  fldgenss  33298  ss2mcls  35553  pclssN  39877  dochspss  41361  clss2lem  43601
  Copyright terms: Public domain W3C validator