Theorem intss 4897

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

Syntax hints:   → wi 4  {cab 2799  ∀wral 3138   ⊆ wss 3936  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-in 3943  df-ss 3952  df-int 4877

This theorem is referenced by:  uniintsn  4913  intabs  5245  fiss  8888  tc2  9184  tcss  9186  tcel  9187  rankval4  9296  cfub  9671  cflm  9672  cflecard  9675  fin23lem26  9747  clsslem  14344  mrcss  16887  lspss  19756  lbsextlem3  19932  aspss  20106  clsss  21662  1stcfb  22053  ufinffr  22537  spanss  29125  ss2mcls  32815  pclssN  37045  dochspss  38529  clss2lem  39991