Theorem ssrin 2237

Description: Add right intersection to subclass relation.

Assertion

Ref	Expression
ssrin	⊢ (A ⊆ B → (A ∩ C) ⊆ (B ∩ C))

Proof of Theorem ssrin

Step	Hyp	Ref	Expression
1		pm3.45 564	. . . 4 ⊢ ((x ∈ A → x ∈ B) → ((x ∈ A ⋀ x ∈ C) → (x ∈ B ⋀ x ∈ C)))
2		elin 2210	. . . 4 ⊢ (x ∈ (A ∩ C) ↔ (x ∈ A ⋀ x ∈ C))
3		elin 2210	. . . 4 ⊢ (x ∈ (B ∩ C) ↔ (x ∈ B ⋀ x ∈ C))
4	1, 2, 3	3imtr4g 555	. . 3 ⊢ ((x ∈ A → x ∈ B) → (x ∈ (A ∩ C) → x ∈ (B ∩ C)))
5	4	19.20i 994	. 2 ⊢ (∀x(x ∈ A → x ∈ B) → ∀x(x ∈ (A ∩ C) → x ∈ (B ∩ C)))
6		dfss2 2061	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
7		dfss2 2061	. 2 ⊢ ((A ∩ C) ⊆ (B ∩ C) ↔ ∀x(x ∈ (A ∩ C) → x ∈ (B ∩ C)))
8	5, 6, 7	3imtr4 219	1 ⊢ (A ⊆ B → (A ∩ C) ⊆ (B ∩ C))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 956   ∈ wcel 960   ∩ cin 2049   ⊆ wss 2050

This theorem is referenced by:  sslin 2238  ss2in 2239  ssdisj 2322  ssres 3391  sbthlem7 4459  phplem2 4515  tgsst 7635  islp2 7744  orthin 9365  3oalem6 9607  mdbr2 10218  mdslle1 10239  mdslle2 10240  mdslj1 10241  mdslj2 10242  mdsl2 10244  mdslmd1lem1 10247  mdslmd1lem2 10248  mdslmd3 10254  mdexch 10257  sumdmdlem 10340

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056

Copyright terms: Public domain