Theorem intss 4921

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

Syntax hints:   → wi 4  {cab 2734  ∀wral 3070   ⊆ wss 3899  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-ral 3071  df-ss 3916  df-int 4900

This theorem is referenced by:  uniintsn  4937  intabs  5299  cofon1  8630  naddssim  8644  fiss  9360  tc2  9685  tcss  9687  tcel  9688  rankval4  9815  cfub  10195  cflm  10196  cflecard  10199  fin23lem26  10272  clsslem  14987  mrcss  17624  lspss  21024  lbsextlem3  21203  aspss  21901  clsss  23087  1stcfb  23478  ufinffr  23962  cofcut1  27983  spanss  31490  fldgenss  33457  rankval4b  35351  ss2mcls  35866  pclssN  40466  dochspss  41950  clss2lem  44135