Theorem ssrdv 3185

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 1885	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3168	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2164   ⊆ wss 3153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  eqelssd  3198  sscon  3293  ssdif  3294  unss1  3328  ssrin  3384  eq0rdv  3491  uniss  3856  intss1  3885  intmin  3890  intssunim  3892  iunss1  3923  iinss1  3924  ss2iun  3927  ssiun  3954  ssiun2  3955  iinss  3964  iinss2  3965  exmidundif  4235  exmidundifim  4236  sspwb  4245  tron  4413  ssorduni  4519  ordsson  4524  ordpwsucss  4599  xpsspw  4771  relop  4812  dmss  4861  dmcosseq  4933  ssrnres  5108  chfnrn  5669  ffnfv  5716  f1imass  5817  fo1stresm  6214  fo2ndresm  6215  oprssdmm  6224  fo2ndf  6280  reldmtpos  6306  smoiun  6354  tfrlemi14d  6386  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemres  6415  dcdifsnid  6557  qsss  6648  pmss12g  6729  mapss  6745  ixpssmap2g  6781  ixpssmapg  6782  en2eqpr  6963  exmidpw  6964  exmidpweq  6965  onunsnss  6973  undifdcss  6979  ssfii  7033  fiss  7036  difinfsn  7159  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  ltprordil  7649  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  aptiprleml  7699  aptiprlemu  7700  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  suplocexprlemss  7775  suplocexprlemex  7782  peano5uzti  9425  uzss  9613  ixxdisj  9969  ixxss1  9970  ixxss2  9971  ixxss12  9972  iocssre  10019  icossre  10020  iccssre  10021  icodisj  10058  fzss1  10129  fzss2  10130  fzoss1  10238  fzosplit  10244  fzouzsplit  10246  ssfzo12bi  10292  frecuzrdgtcl  10483  frecuzrdgdomlem  10488  sswrd  10923  ovshftex  10963  summodclem2a  11524  fsum3cvg3  11539  fsum2dlemstep  11577  prodmodclem2a  11719  fprod2dlemstep  11765  phimullem  12363  1arith  12505  ennnfonelemdm  12577  trivsubgsnd  13271  ssnmz  13281  trivnsgd  13287  kerf1ghm  13344  conjnmz  13349  unitssd  13605  subrguss  13732  unitrrg  13763  lsssssubg  13874  lssintclm  13880  zsssubrg  14073  mulgrhm2  14098  znrrg  14148  psrbaglesuppg  14158  bastg  14229  tgss  14231  tgtop  14236  tgidm  14242  neisspw  14316  topssnei  14330  tgrest  14337  ssrest  14350  cnss1  14394  cnss2  14395  cnsscnp  14397  cnrest2r  14405  txdis  14445  xblss2ps  14572  xblss2  14573  xmettxlem  14677  xmettx  14678  cncfss  14738  cnopnap  14765  dvfgg  14842  dvcj  14858