Theorem ssrdv 2073

Description: Deduction rule based on subclass definition.

Hypothesis

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

Assertion

Ref	Expression
ssrdv	|- (ph -> A (_ B)

Distinct variable groups:   x,A   x,B   ph,x

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 |- (ph -> (x e. A -> x e. B))
2	1	19.21aiv 1288	. 2 |- (ph -> A.x(x e. A -> x e. B))
3		dfss2 2061	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
4	2, 3	sylibr 200	1 |- (ph -> A (_ B)

Syntax hints:   -> wi 3  A.wal 956   e. wcel 960   (_ wss 2050

This theorem is referenced by:  sscon 2174  ssdif 2175  difsn 2468  prss 2475  tpss 2480  intss1 2552  intmin 2557  intssuni 2559  ss2iun 2581  ssiun2 2597  sspwb 2761  pwssun 2833  tz7.7 2979  ordon 2993  ssorduni 2999  onint 3012  limsssuc 3127  limuni3 3129  limomss 3143  relop 3281  dmss 3316  ssrnres 3487  chfnrn 3808  dff2 3823  tz7.48-1 3962  tz7.49 3965  oaass 4201  ss2ixp 4360  mapenlem2 4496  pssnn 4544  inf3lemd 4621  inf3lem1 4622  inf3lem6 4627  r1tr 4664  zorn2lem4 4801  zorn2lem5 4802  unxpdomlem 4854  carduni 4869  genpss 5119  distrlem1pr 5139  distrlem5pr 5143  ltexprlem2 5155  ltexprlem6 5159  ltexprlem7 5160  reclem3pr 5170  reclem4pr 5171  suppsrlem 5233  suprelem 5271  iccssret 6397  uzss 6432  infxpidmlem7 7559  infxpidmlem8 7560  bastgt 7621  tgtopt 7627  tgsst 7635  tgss2t 7636  basgen2t 7638  clslp 7745  cnsscnp 7769  cncnplem2 7772  ssbl 7852  blssopn 7864  unirnbl 7872  metcnss 7895  cmsss 7994  grplactf1o 8094  ubthlem2 8526  psdmrn 8644  ococss 9161  shsub1t 9283  shless 9342  shmods 9357  spansnsst 9489  spanpr 9498  spansnm0 9590  pjjs 9640  sumdmdi 10337  sumdmdlem 10340  sumdmdlem2 10341  cdj3lem1 10356  uninqs 10436  clsrebb 10479  rdmob 10652  rcmob 10653

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain