Theorem ssrdv 3020

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

Hypothesis

Ref	Expression
ssrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
ssrdv	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1799	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3003	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 132	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1285   ∈ wcel 1436   ⊆ wss 2988

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001

This theorem is referenced by:  sscon  3123  ssdif  3124  unss1  3158  ssrin  3214  eq0rdv  3315  uniss  3659  intss1  3688  intmin  3693  intssunim  3695  iunss1  3726  iinss1  3727  ss2iun  3730  ssiun  3757  ssiun2  3758  iinss  3766  iinss2  3767  trintssmOLD  3930  exmidundif  4011  sspwb  4019  tron  4185  ssorduni  4279  ordsson  4284  ordpwsucss  4358  xpsspw  4520  relop  4556  dmss  4605  dmcosseq  4674  ssrnres  4841  chfnrn  5375  ffnfv  5421  f1imass  5516  fo1stresm  5891  fo2ndresm  5892  fo2ndf  5951  reldmtpos  5974  smoiun  6022  tfrlemi14d  6054  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemres  6083  dcdifsnid  6219  qsss  6305  pmss12g  6386  mapss  6402  en2eqpr  6577  exmidpw  6578  onunsnss  6581  undifdcss  6587  addnqprlemrl  7063  addnqprlemru  7064  addnqprlemfl  7065  addnqprlemfu  7066  mulnqprlemrl  7079  mulnqprlemru  7080  mulnqprlemfl  7081  mulnqprlemfu  7082  distrlem1prl  7088  distrlem1pru  7089  distrlem5prl  7092  distrlem5pru  7093  ltprordil  7095  ltexprlemfl  7115  ltexprlemrl  7116  ltexprlemfu  7117  ltexprlemru  7118  addcanprleml  7120  addcanprlemu  7121  recexprlem1ssl  7139  recexprlem1ssu  7140  recexprlemss1l  7141  recexprlemss1u  7142  aptiprleml  7145  aptiprlemu  7146  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  peano5uzti  8790  uzss  8974  ixxdisj  9256  ixxss1  9257  ixxss2  9258  ixxss12  9259  iocssre  9306  icossre  9307  iccssre  9308  icodisj  9344  fzss1  9411  fzss2  9412  fzoss1  9513  fzosplit  9519  fzouzsplit  9521  ssfzo12bi  9567  frecuzrdgtcl  9750  frecuzrdgdomlem  9755  ovshftex  10171  isummolem2a  10684  fisumcvg3  10698  phimullem  11126