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

Theorem ssriv 3071
Description: Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
ssriv.1  |-  ( x  e.  A  ->  x  e.  B )
Assertion
Ref Expression
ssriv  |-  A  C_  B
Distinct variable groups:    x, A    x, B

Proof of Theorem ssriv
StepHypRef Expression
1 dfss2 3056 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 ssriv.1 . 2  |-  ( x  e.  A  ->  x  e.  B )
31, 2mpgbir 1414 1  |-  A  C_  B
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465    C_ wss 3041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  ssid  3087  ssv  3089  difss  3172  ssun1  3209  inss1  3266  unssdif  3281  inssdif  3282  unssin  3285  inssun  3286  difindiss  3300  undif3ss  3307  0ss  3371  difprsnss  3628  snsspw  3661  pwprss  3702  pwtpss  3703  uniin  3726  iuniin  3793  iundif2ss  3848  iunpwss  3874  pwuni  4086  pwunss  4175  omsson  4496  limom  4497  xpsspw  4621  dmin  4717  dmrnssfld  4772  dmcoss  4778  dminss  4923  imainss  4924  dmxpss  4939  rnxpid  4943  mapsspm  6544  pmsspw  6545  uniixp  6583  snexxph  6806  djuss  6923  enq0enq  7207  nqnq0pi  7214  nqnq0  7217  apsscn  8377  sup3exmid  8683  zssre  9029  zsscn  9030  nnssz  9039  uzssz  9313  divfnzn  9381  zssq  9387  qssre  9390  rpssre  9420  ixxssxr  9651  ixxssixx  9653  iooval2  9666  ioossre  9686  rge0ssre  9728  fz1ssnn  9804  fzssuz  9813  fzssp1  9815  uzdisj  9841  fz0ssnn0  9864  nn0disj  9883  fzossfz  9910  fzouzsplit  9924  fzossnn  9934  fzo0ssnn0  9960  seq3coll  10553  fclim  11031  infssuzcldc  11571  prmssnn  11720  restsspw  12057  unitg  12158  cldss2  12202  blssioo  12641  tgioo  12642  limccl  12724  limcresi  12731  dvef  12783  bj-omsson  13087
  Copyright terms: Public domain W3C validator