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

Theorem ssriv 2949
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 2934 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1342 1 𝐴𝐵
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  wss 2917
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931
This theorem is referenced by:  ssid  2964  ssv  2965  difss  3070  ssun1  3106  inss1  3157  unssdif  3172  inssdif  3173  unssin  3176  inssun  3177  difindiss  3191  undif3ss  3198  0ss  3255  difprsnss  3502  snsspw  3535  pwprss  3576  pwtpss  3577  uniin  3600  iuniin  3667  iundif2ss  3722  iunpwss  3743  pwuni  3943  pwunss  4020  omsson  4335  limom  4336  xpsspw  4450  dmin  4543  dmrnssfld  4595  dmcoss  4601  dminss  4738  imainss  4739  dmxpss  4753  rnxpid  4755  enq0enq  6527  nqnq0pi  6534  nqnq0  6537  zssre  8250  zsscn  8251  nnssz  8260  uzssz  8490  divfnzn  8554  zssq  8560  qssre  8563  rpssre  8591  ixxssxr  8767  ixxssixx  8769  iooval2  8782  ioossre  8802  rge0ssre  8844  fzssuz  8926  fzssp1  8928  uzdisj  8953  nn0disj  8993  fzossfz  9019  fzouzsplit  9033  fzossnn  9043  fzo0ssnn0  9069  fclim  9789  bj-omsson  10061
  Copyright terms: Public domain W3C validator