Theorem ssriv 2059

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 2048	. 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 985	1 |- A (_ B

Syntax hints:   -> wi 3   e. wcel 955   (_ wss 2037

This theorem is referenced by:  ssv 2071  difss 2157  ssun1 2183  inss1 2220  0ss 2291  difprsn 2456  snsspw 2470  uniin 2510  iuniin 2563  iunpwss 2608  unipw 2746  pwuni 2747  pwunss 2815  omsson 3126  omssnlim 3135  xpss 3220  dmin 3307  dmrnssfld 3343  dminss 3448  imainss 3449  mapsspm 4323  uniixp 4341  ixpssmap 4347  abfii3 4537  pwfilem 4544  dfom3 4602  tz9.12lem1 4631  rankun 4663  alephsson 4866  cardcf 4883  cfeq0 4886  1pr 5089  reclem2pr 5129  zssre 6089  zsscn 6090  nnssz 6098  zssq 6199  qssre 6202  rpssre 6223  ioossicc 6330  fzssuzt 6437  ivthlem4OLD 7228  ivthOLD 7233  ivth2OLD 7234  reeff1olem1 7364  reeff1olem1OLD 7366  reeff1o 7368  subbas2 7587  ntrss2 7632  qdensere 7691  blssioo 7852  tgioo 7854  sspval 8316  phrel 8405  bnrel 8458  ubthlem6 8465  hlrel 8525  pilem2 8591  efifolem4 8640  eff1i 8665  effoi 8666  effoiOLD 8667  resslogrn 8675  chsscm 9033  chcmh 9034  hhssnv 9054  omlsi 9160  choc1 9206  shunss 9252  shslej 9253  shsub1 9256  shsub2 9257  shsidm 9272  spanun 9382  spansn 9396  5oalem7 9522  3oalem3 9526  mayete3 9590  hmopex 9719  cnlnssadj 9928  adjbdlnt 9931  adjsslnop 9935  shatomistic 10196  hatomistic 10197

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain