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

Theorem intss 4888
 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 4031 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝑦𝑥 → ∀𝑥𝐴 𝑦𝑥))
21ss2abdv 4042 . 2 (𝐴𝐵 → {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥} ⊆ {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥})
3 dfint2 4869 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
4 dfint2 4869 . 2 𝐴 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝑥}
52, 3, 43sstr4g 4010 1 (𝐴𝐵 𝐵 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  {cab 2797  ∀wral 3136   ⊆ wss 3934  ∩ cint 4867 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-in 3941  df-ss 3950  df-int 4868 This theorem is referenced by:  uniintsn  4904  intabs  5236  fiss  8880  tc2  9176  tcss  9178  tcel  9179  rankval4  9288  cfub  9663  cflm  9664  cflecard  9667  fin23lem26  9739  clsslem  14336  mrcss  16879  lspss  19748  lbsextlem3  19924  aspss  20098  clsss  21654  1stcfb  22045  ufinffr  22529  spanss  29117  ss2mcls  32808  pclssN  37022  dochspss  38506  clss2lem  39962
 Copyright terms: Public domain W3C validator