Theorem intss 4900

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.

Step	Hyp	Ref	Expression
1		ssralv 3987	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥))
2	1	ss2abdv 3997	. 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥})
3		dfint2 4881	. 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
4		dfint2 4881	. 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
5	2, 3, 4	3sstr4g 3966	1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)

Syntax hints:   → wi 4  {cab 2715  ∀wral 3064   ⊆ wss 3887  ∩ cint 4879

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-int 4880

This theorem is referenced by:  uniintsn  4918  intabs  5266  fiss  9183  tc2  9500  tcss  9502  tcel  9503  rankval4  9625  cfub  10005  cflm  10006  cflecard  10009  fin23lem26  10081  clsslem  14695  mrcss  17325  lspss  20246  lbsextlem3  20422  aspss  21081  clsss  22205  1stcfb  22596  ufinffr  23080  spanss  29710  ss2mcls  33530  naddssim  33837  cofcut1  34090  pclssN  37908  dochspss  39392  clss2lem  41219