Theorem ssrdv 3231

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

Syntax hints:   → wi 4  ∀wal 1393   ∈ wcel 2200   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqelssd  3244  sscon  3339  ssdif  3340  unss1  3374  ssrin  3430  eq0rdv  3537  uniss  3912  intss1  3941  intmin  3946  intssunim  3948  iunss1  3979  iinss1  3980  ss2iun  3983  ssiun  4010  ssiun2  4011  iinss  4020  iinss2  4021  exmidundif  4294  exmidundifim  4295  sspwb  4306  tron  4477  ssorduni  4583  ordsson  4588  ordpwsucss  4663  xpsspw  4836  relop  4878  dmss  4928  dmcosseq  5002  ssrnres  5177  chfnrn  5754  ffnfv  5801  f1imass  5910  fo1stresm  6319  fo2ndresm  6320  oprssdmm  6329  fo2ndf  6387  reldmtpos  6414  smoiun  6462  tfrlemi14d  6494  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemres  6523  dcdifsnid  6667  qsss  6758  pmss12g  6839  mapss  6855  ixpssmap2g  6891  ixpssmapg  6892  en2eqpr  7092  exmidpw  7093  exmidpweq  7094  onunsnss  7102  undifdcss  7108  ssfii  7164  fiss  7167  difinfsn  7290  addnqprlemrl  7767  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemrl  7783  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  distrlem1prl  7792  distrlem1pru  7793  distrlem5prl  7796  distrlem5pru  7797  ltprordil  7799  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  aptiprleml  7849  aptiprlemu  7850  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  suplocexprlemss  7925  suplocexprlemex  7932  peano5uzti  9578  uzss  9767  ixxdisj  10128  ixxss1  10129  ixxss2  10130  ixxss12  10131  iocssre  10178  icossre  10179  iccssre  10180  icodisj  10217  fzss1  10288  fzss2  10289  fzoss1  10398  fzosplit  10404  fzouzsplit  10406  ssfzo12bi  10460  frecuzrdgtcl  10664  frecuzrdgdomlem  10669  sswrd  11112  ovshftex  11370  summodclem2a  11932  fsum3cvg3  11947  fsum2dlemstep  11985  prodmodclem2a  12127  fprod2dlemstep  12173  bitsfzo  12506  phimullem  12787  1arith  12930  ennnfonelemdm  13031  trivsubgsnd  13778  ssnmz  13788  trivnsgd  13794  kerf1ghm  13851  conjnmz  13856  unitssd  14113  subrguss  14240  unitrrg  14271  lsssssubg  14382  lssintclm  14388  zsssubrg  14589  mulgrhm2  14614  znrrg  14664  psrbaglesuppg  14676  bastg  14775  tgss  14777  tgtop  14782  tgidm  14788  neisspw  14862  topssnei  14876  tgrest  14883  ssrest  14896  cnss1  14940  cnss2  14941  cnsscnp  14943  cnrest2r  14951  txdis  14991  xblss2ps  15118  xblss2  15119  xmettxlem  15223  xmettx  15224  cncfss  15297  cnopnap  15325  dvfgg  15402  dvcj  15423  usgruspgrben  16025