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

Theorem ssriv 3069
Description: Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
ssriv.1 (𝑥𝐴𝑥𝐵)
Assertion
Ref Expression
ssriv 𝐴𝐵
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssriv
StepHypRef Expression
1 dfss2 3054 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1412 1 𝐴𝐵
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  ssid  3085  ssv  3087  difss  3170  ssun1  3207  inss1  3264  unssdif  3279  inssdif  3280  unssin  3283  inssun  3284  difindiss  3298  undif3ss  3305  0ss  3369  difprsnss  3626  snsspw  3659  pwprss  3700  pwtpss  3701  uniin  3724  iuniin  3791  iundif2ss  3846  iunpwss  3872  pwuni  4084  pwunss  4173  omsson  4494  limom  4495  xpsspw  4619  dmin  4715  dmrnssfld  4770  dmcoss  4776  dminss  4921  imainss  4922  dmxpss  4937  rnxpid  4941  mapsspm  6542  pmsspw  6543  uniixp  6581  snexxph  6804  djuss  6921  enq0enq  7203  nqnq0pi  7210  nqnq0  7213  apsscn  8371  sup3exmid  8672  zssre  9012  zsscn  9013  nnssz  9022  uzssz  9294  divfnzn  9362  zssq  9368  qssre  9371  rpssre  9400  ixxssxr  9623  ixxssixx  9625  iooval2  9638  ioossre  9658  rge0ssre  9700  fz1ssnn  9776  fzssuz  9785  fzssp1  9787  uzdisj  9813  fz0ssnn0  9836  nn0disj  9855  fzossfz  9882  fzouzsplit  9896  fzossnn  9906  fzo0ssnn0  9932  seq3coll  10525  fclim  11003  infssuzcldc  11540  prmssnn  11689  restsspw  12025  unitg  12126  cldss2  12170  blssioo  12609  tgioo  12610  limccl  12680  limcresi  12687  dvef  12739  bj-omsson  12971
  Copyright terms: Public domain W3C validator