Theorem intss 4933

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 4005	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥))
2	1	ss2abdv 4018	. 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} ⊆ {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥})
3		dfint2 4913	. 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
4		dfint2 4913	. 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
5	2, 3, 4	3sstr4g 3989	1 ⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)

Syntax hints:   → wi 4  {cab 2739  ∀wral 3077   ⊆ wss 3904  ∩ cint 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-ral 3078  df-ss 3921  df-int 4912

This theorem is referenced by:  uniintsn  4949  intabs  5319  cofon1  8657  naddssim  8671  fiss  9383  tc2  9708  tcss  9710  tcel  9711  rankval4  9838  cfub  10231  cflm  10232  cflecard  10235  fin23lem26  10308  clsslem  15021  mrcss  17671  lspss  21084  lbsextlem3  21263  aspss  22005  clsss  23190  1stcfb  23581  ufinffr  24065  cofcut1  28089  spanss  31666  fldgenss  33603  rankval4b  35459  ss2mcls  36026  pclssN  40636  dochspss  42120  clss2lem  44307