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

Theorem intss 4650
 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 3807 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝑦𝑥 → ∀𝑥𝐴 𝑦𝑥))
21ss2abdv 3816 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4629 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4629 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 3787 1 (𝐴𝐵 𝐵 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  {cab 2746  ∀wral 3050   ⊆ wss 3715  ∩ cint 4627 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-in 3722  df-ss 3729  df-int 4628 This theorem is referenced by:  uniintsn  4666  intabs  4974  fiss  8495  tc2  8791  tcss  8793  tcel  8794  rankval4  8903  cfub  9263  cflm  9264  cflecard  9267  fin23lem26  9339  clsslem  13924  mrcss  16478  lspss  19186  lbsextlem3  19362  aspss  19534  clsss  21060  1stcfb  21450  ufinffr  21934  spanss  28516  ss2mcls  31772  pclssN  35683  dochspss  37169  clss2lem  38420
 Copyright terms: Public domain W3C validator