Theorem ssrdv 2070

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 1286	. 2 |- (ph -> A.x(x e. A -> x e. B))
3		dfss2 2058	. 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 954   e. wcel 958   (_ wss 2047

This theorem is referenced by:  sscon 2171  ssdif 2172  difsn 2464  prss 2471  tpss 2476  intss1 2548  intmin 2553  intssuni 2555  ss2iun 2577  ssiun2 2593  sspwb 2755  pwssun 2827  tz7.7 2973  ordon 2987  ssorduni 2993  onint 3006  limsssuc 3121  limuni3 3123  limomss 3137  relop 3275  dmss 3310  ssrnres 3481  chfnrn 3802  dff2 3817  tz7.48-1 3956  tz7.49 3959  oaass 4195  ss2ixp 4354  mapenlem2 4490  pssnn 4534  inf3lemd 4612  inf3lem1 4613  inf3lem6 4618  r1tr 4654  zorn2lem4 4791  zorn2lem5 4792  unxpdomlem 4843  carduni 4858  genpss 5107  distrlem1pr 5127  distrlem5pr 5131  ltexprlem2 5143  ltexprlem6 5147  ltexprlem7 5148  reclem3pr 5158  reclem4pr 5159  suppsrlem 5221  suprelem 5259  iccssret 6396  uzss 6431  infxpidmlem7 7558  infxpidmlem8 7559  bastgt 7622  tgtopt 7628  tgsst 7636  tgss2t 7637  basgen2t 7639  clslp 7748  cnsscnp 7772  cncnplem2 7775  ssbl 7855  blssopn 7867  unirnbl 7875  metcnss 7898  cmsss 7997  grplactf1o 8098  ubthlem2 8530  psdmrn 8648  ococss 9166  shsub1t 9288  shless 9347  shmods 9362  spansnsst 9494  spanpr 9503  spansnm0 9595  pjjs 9645  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346  cdj3lem1 10361  uninqs 10441  clsrebb 10493  rdmob 10681  rcmob 10682

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