Theorem intss 4928

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

This proof depends on syntax axioms:   → wi 4  {cab 2738  ∀wral 3076   ⊆ wss 3895  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-ss 3896  df-int 4907

This theorem is used by:  uniintsn  4944  intabs  5309  cofon1  8682  naddssim  8696  fiss  9417  tc2  9742  tcss  9744  tcel  9745  rankval4b  9881  rankval4  9885  cfub  10327  cflm  10328  cflecard  10331  fin23lem26  10404  clsslem  15138  mrcss  17791  lspss  21260  lbsextlem3  21439  aspss  22185  clsss  23373  1stcfb  23764  ufinffr  24249  cofcut1  28307  spanss  31951  fldgenss  33921  ss2mcls  36402  pclssN  41027  dochspss  42511  clss2lem  44687