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

Theorem ssriv 2974
Description: Inference rule 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 2959 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1356 1 𝐴𝐵
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1407  wss 2942
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-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-11 1411  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-in 2949  df-ss 2956
This theorem is referenced by:  ssid  2989  ssv  2990  difss  3095  ssun1  3131  inss1  3182  unssdif  3197  inssdif  3198  unssin  3201  inssun  3202  difindiss  3216  undif3ss  3223  0ss  3280  difprsnss  3527  snsspw  3560  pwprss  3601  pwtpss  3602  uniin  3625  iuniin  3692  iundif2ss  3747  iunpwss  3768  pwuni  3968  pwunss  4045  omsson  4360  limom  4361  xpsspw  4475  dmin  4568  dmrnssfld  4620  dmcoss  4626  dminss  4763  imainss  4764  dmxpss  4778  rnxpid  4780  enq0enq  6557  nqnq0pi  6564  nqnq0  6567  zssre  8279  zsscn  8280  nnssz  8289  uzssz  8558  divfnzn  8623  zssq  8629  qssre  8632  rpssre  8661  ixxssxr  8840  ixxssixx  8842  iooval2  8855  ioossre  8875  rge0ssre  8917  fzssuz  9000  fzssp1  9002  uzdisj  9027  nn0disj  9067  fzossfz  9093  fzouzsplit  9107  fzossnn  9117  fzo0ssnn0  9143  fclim  10009  bj-omsson  10417
  Copyright terms: Public domain W3C validator