Theorem ssrdv 1509

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 group(s):   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 943	. 2 |- (ph -> A.x(x e. A -> x e. B))
3		dfss2 1497	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
4	2, 3	sylibr 175	1 |- (ph -> A (_ B)

Syntax hints:   -> wi 2  A.wal 672   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  sscon 1599  ssdif 1600  prss 1854  tpss 1855  sspwb 1863  pwssun 1917  intss1 1979  intmin 1982  ss2iun 2005  ssiun2 2019  tz7.7 2224  ordon 2238  ssorduni 2249  onint 2261  limsssuc 2362  limomss 2378  dmss 2530  chfnrn 2885  tz7.48-1 2994  tz7.49 2997  oaass 3163  mapenlem2 3385  pssnn 3428  inf3lemd 3463  inf3lem1 3464  inf3lem6 3469  r1tr 3498  zornlem4 3606  zornlem5 3607  unxpdomlem 3649  carduni 3664  genpss 3901  distrlem1pr 3921  distrlem5pr 3925  ltexprlem2 3937  ltexprlem6 3941  ltexprlem7 3942  reclem3pr 3952  reclem4pr 3953  suppsrlem 4015  suprelem 4053  infxpidmlem7 4939  infxpidmlem8 4940  ococss 5174  pjoml 5271  shsub1t 5289  shless 5348  shmods 5363  spansnsst 5476  pjjs 5585  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org