Theorem ssrdv 2924

Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
ssrdv.1	⊢ (φ → (x ∈ A → x ∈ B))

Assertion

Ref	Expression
ssrdv	⊢ (φ → A ⊆ B)

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

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (φ → (x ∈ A → x ∈ B))
2	1	alrimiv 1732	. 2 ⊢ (φ → ∀x(x ∈ A → x ∈ B))
3		dfss2 2907	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4	2, 3	sylibr 137	1 ⊢ (φ → A ⊆ B)

Syntax hints:   → wi 4  ∀wal 1224   ∈ wcel 1370   ⊆ wss 2890

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-in 2897  df-ss 2904

This theorem is referenced by:  sscon  3050  ssdif  3051  unss1  3085  ssrin  3135  eq0rdv  3234  uniss  3571  intss1  3600  intmin  3605  intssunim  3607  iunss1  3638  iinss1  3639  ss2iun  3642  ssiun  3669  ssiun2  3670  iinss  3678  iinss2  3679  trintssm  3840  sspwb  3922  tron  4064  ssorduni  4159  ordsson  4164  ordpwsucss  4223  xpsspw  4373  relop  4409  dmss  4457  dmcosseq  4526  ssrnres  4686  chfnrn  5199  ffnfv  5244  f1imass  5334  fo1stresm  5707  fo2ndresm  5708  fo2ndf  5767  reldmtpos  5786  smoiun  5834  tfrlemi14d  5864  qsss  6072  distrlem1prl  6415  distrlem1pru  6416  distrlem5prl  6419  distrlem5pru  6420  ltprordil  6422  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  recexprlem1ssl  6461  recexprlem1ssu  6462  recexprlemss1l  6463  recexprlemss1u  6464