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

Theorem intss 4968
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 4065 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4947 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4947 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 4036 1 (𝐴𝐵 𝐵 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2713  wral 3060  wss 3950   cint 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-ral 3061  df-ss 3967  df-int 4946
This theorem is referenced by:  uniintsn  4984  intabs  5348  cofon1  8711  naddssim  8724  fiss  9465  tc2  9783  tcss  9785  tcel  9786  rankval4  9908  cfub  10290  cflm  10291  cflecard  10294  fin23lem26  10366  clsslem  15024  mrcss  17660  lspss  20983  lbsextlem3  21163  aspss  21898  clsss  23063  1stcfb  23454  ufinffr  23938  cofcut1  27955  spanss  31368  fldgenss  33319  ss2mcls  35574  pclssN  39897  dochspss  41381  clss2lem  43629
  Copyright terms: Public domain W3C validator