Theorem ssriv 2069

Description: Inference rule based on subclass definition.

Hypothesis

Ref	Expression
ssriv.1	|- (x e. A -> x e. B)

Assertion

Ref	Expression
ssriv	|- A (_ B

Distinct variable groups:   x,A   x,B

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 2058	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		ssriv.1	. 2 |- (x e. A -> x e. B)
3	1, 2	mpgbir 988	1 |- A (_ B

Syntax hints:   -> wi 3   e. wcel 958   (_ wss 2047

This theorem is referenced by:  ssv 2081  difss 2167  ssun1 2193  inss1 2230  0ss 2301  difprsn 2465  snsspw 2479  uniin 2520  iuniin 2573  iunpwss 2618  unipw 2756  pwuni 2757  pwunss 2826  omsson 3136  omssnlim 3145  xpss 3230  dmin 3318  dmrnssfld 3357  dminss 3462  imainss 3463  mapsspm 4339  uniixp 4357  ixpssmap 4363  abfii3OLD 4563  pwfilemOLD 4570  dfom3 4630  tz9.12lem1 4659  rankun 4691  alephsson 4894  cardcf 4911  cfeq0 4914  1pr 5117  reclem2pr 5157  zssre 6142  zsscn 6143  nnssz 6151  zssq 6261  qssre 6264  rpssre 6285  ioossre 6389  ioossicc 6397  fzssuzt 6505  reeff1olem1 7424  reeff1o 7426  subbas2OLD 7645  ntrss2 7690  qdensere 7751  blssioo 7913  tgioo 7915  sspval 8382  phrel 8474  bnrel 8527  ubthlem6 8534  hlrel 8594  pilem2 8672  efifolem4 8725  eff1i 8744  effoi 8745  resslogrn 8753  chsscm 9112  chcmh 9113  hhssnv 9134  omlsi 9245  choc1 9291  shunss 9337  shslej 9338  shsub1 9341  shsub2 9342  shsidm 9357  spanun 9467  spansn 9480  5oalem7 9605  3oalem3 9609  mayete3 9673  hmopex 9802  cnlnssadj 10013  adjbdlnt 10016  adjsslnop 10020  shatomistic 10288  hatomistic 10289

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain