Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  inss1 GIF version

Theorem inss1 3185
 Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
inss1 (𝐴𝐵) ⊆ 𝐴

Proof of Theorem inss1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3154 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21simplbi 263 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
32ssriv 2977 1 (𝐴𝐵) ⊆ 𝐴
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1409   ∩ cin 2944   ⊆ wss 2945 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952  df-ss 2959 This theorem is referenced by:  inss2  3186  ssinss1  3193  unabs  3195  nssinpss  3197  inssddif  3206  inv1  3281  disjdif  3324  inundifss  3329  relin1  4483  resss  4663  resmpt3  4685  cnvcnvss  4803  funin  4998  funimass2  5005  fnresin1  5041  fnres  5043  fresin  5096  ssimaex  5262  fneqeql2  5304  isoini2  5486  ofrfval  5748  fnofval  5749  ofrval  5750  off  5752  ofres  5753  ofco  5757  smores  5938  smores2  5940  tfrlem5  5961  peano5nnnn  7024  peano5nni  7993  rexanuz  9815
 Copyright terms: Public domain W3C validator