Theorem ssrdv 3153

Description: Deduction 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 1867	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3136	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 133	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1346   ∈ wcel 2141   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqelssd  3166  sscon  3261  ssdif  3262  unss1  3296  ssrin  3352  eq0rdv  3459  uniss  3817  intss1  3846  intmin  3851  intssunim  3853  iunss1  3884  iinss1  3885  ss2iun  3888  ssiun  3915  ssiun2  3916  iinss  3924  iinss2  3925  exmidundif  4192  exmidundifim  4193  sspwb  4201  tron  4367  ssorduni  4471  ordsson  4476  ordpwsucss  4551  xpsspw  4723  relop  4761  dmss  4810  dmcosseq  4882  ssrnres  5053  chfnrn  5607  ffnfv  5654  f1imass  5753  fo1stresm  6140  fo2ndresm  6141  oprssdmm  6150  fo2ndf  6206  reldmtpos  6232  smoiun  6280  tfrlemi14d  6312  tfr1onlemres  6328  tfri1dALT  6330  tfrcllemres  6341  dcdifsnid  6483  qsss  6572  pmss12g  6653  mapss  6669  ixpssmap2g  6705  ixpssmapg  6706  en2eqpr  6885  exmidpw  6886  exmidpweq  6887  onunsnss  6894  undifdcss  6900  ssfii  6951  fiss  6954  difinfsn  7077  addnqprlemrl  7519  addnqprlemru  7520  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemrl  7535  mulnqprlemru  7536  mulnqprlemfl  7537  mulnqprlemfu  7538  distrlem1prl  7544  distrlem1pru  7545  distrlem5prl  7548  distrlem5pru  7549  ltprordil  7551  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  aptiprleml  7601  aptiprlemu  7602  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  suplocexprlemss  7677  suplocexprlemex  7684  peano5uzti  9320  uzss  9507  ixxdisj  9860  ixxss1  9861  ixxss2  9862  ixxss12  9863  iocssre  9910  icossre  9911  iccssre  9912  icodisj  9949  fzss1  10019  fzss2  10020  fzoss1  10127  fzosplit  10133  fzouzsplit  10135  ssfzo12bi  10181  frecuzrdgtcl  10368  frecuzrdgdomlem  10373  ovshftex  10783  summodclem2a  11344  fsum3cvg3  11359  fsum2dlemstep  11397  prodmodclem2a  11539  fprod2dlemstep  11585  phimullem  12179  1arith  12319  ennnfonelemdm  12375  bastg  12855  tgss  12857  tgtop  12862  tgidm  12868  neisspw  12942  topssnei  12956  tgrest  12963  ssrest  12976  cnss1  13020  cnss2  13021  cnsscnp  13023  cnrest2r  13031  txdis  13071  xblss2ps  13198  xblss2  13199  xmettxlem  13303  xmettx  13304  cncfss  13364  cnopnap  13388  dvfgg  13451  dvcj  13467