Theorem ssrdv 3032

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

Syntax hints:   → wi 4  ∀wal 1288   ∈ wcel 1439   ⊆ wss 3000

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013

This theorem is referenced by:  sscon  3135  ssdif  3136  unss1  3170  ssrin  3226  eq0rdv  3331  uniss  3680  intss1  3709  intmin  3714  intssunim  3716  iunss1  3747  iinss1  3748  ss2iun  3751  ssiun  3778  ssiun2  3779  iinss  3787  iinss2  3788  trintssmOLD  3959  exmidundif  4043  exmidundifim  4044  sspwb  4052  tron  4218  ssorduni  4317  ordsson  4322  ordpwsucss  4396  xpsspw  4563  relop  4599  dmss  4648  dmcosseq  4717  ssrnres  4886  chfnrn  5424  ffnfv  5470  f1imass  5567  fo1stresm  5946  fo2ndresm  5947  fo2ndf  6006  reldmtpos  6032  smoiun  6080  tfrlemi14d  6112  tfr1onlemres  6128  tfri1dALT  6130  tfrcllemres  6141  dcdifsnid  6277  qsss  6365  pmss12g  6446  mapss  6462  ixpssmap2g  6498  ixpssmapg  6499  en2eqpr  6677  exmidpw  6678  onunsnss  6681  undifdcss  6687  addnqprlemrl  7170  addnqprlemru  7171  addnqprlemfl  7172  addnqprlemfu  7173  mulnqprlemrl  7186  mulnqprlemru  7187  mulnqprlemfl  7188  mulnqprlemfu  7189  distrlem1prl  7195  distrlem1pru  7196  distrlem5prl  7199  distrlem5pru  7200  ltprordil  7202  ltexprlemfl  7222  ltexprlemrl  7223  ltexprlemfu  7224  ltexprlemru  7225  addcanprleml  7227  addcanprlemu  7228  recexprlem1ssl  7246  recexprlem1ssu  7247  recexprlemss1l  7248  recexprlemss1u  7249  aptiprleml  7252  aptiprlemu  7253  cauappcvgprlemladdfu  7267  cauappcvgprlemladdfl  7268  cauappcvgprlemladdru  7269  cauappcvgprlemladdrl  7270  caucvgprlemladdfu  7290  caucvgprlemladdrl  7291  peano5uzti  8908  uzss  9093  ixxdisj  9375  ixxss1  9376  ixxss2  9377  ixxss12  9378  iocssre  9425  icossre  9426  iccssre  9427  icodisj  9463  fzss1  9531  fzss2  9532  fzoss1  9636  fzosplit  9642  fzouzsplit  9644  ssfzo12bi  9690  frecuzrdgtcl  9873  frecuzrdgdomlem  9878  ovshftex  10307  isummolem2a  10825  fsum3cvg3  10843  fsum2dlemstep  10882  phimullem  11533  bastg  11815  tgss  11817  tgtop  11822  tgidm  11828  cncfss  11905