Theorem ssrdv 3190

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

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqelssd  3203  sscon  3298  ssdif  3299  unss1  3333  ssrin  3389  eq0rdv  3496  uniss  3861  intss1  3890  intmin  3895  intssunim  3897  iunss1  3928  iinss1  3929  ss2iun  3932  ssiun  3959  ssiun2  3960  iinss  3969  iinss2  3970  exmidundif  4240  exmidundifim  4241  sspwb  4250  tron  4418  ssorduni  4524  ordsson  4529  ordpwsucss  4604  xpsspw  4776  relop  4817  dmss  4866  dmcosseq  4938  ssrnres  5113  chfnrn  5676  ffnfv  5723  f1imass  5824  fo1stresm  6228  fo2ndresm  6229  oprssdmm  6238  fo2ndf  6294  reldmtpos  6320  smoiun  6368  tfrlemi14d  6400  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemres  6429  dcdifsnid  6571  qsss  6662  pmss12g  6743  mapss  6759  ixpssmap2g  6795  ixpssmapg  6796  en2eqpr  6977  exmidpw  6978  exmidpweq  6979  onunsnss  6987  undifdcss  6993  ssfii  7049  fiss  7052  difinfsn  7175  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  distrlem1prl  7668  distrlem1pru  7669  distrlem5prl  7672  distrlem5pru  7673  ltprordil  7675  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  aptiprleml  7725  aptiprlemu  7726  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  suplocexprlemss  7801  suplocexprlemex  7808  peano5uzti  9453  uzss  9641  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iocssre  10047  icossre  10048  iccssre  10049  icodisj  10086  fzss1  10157  fzss2  10158  fzoss1  10266  fzosplit  10272  fzouzsplit  10274  ssfzo12bi  10320  frecuzrdgtcl  10523  frecuzrdgdomlem  10528  sswrd  10963  ovshftex  11003  summodclem2a  11565  fsum3cvg3  11580  fsum2dlemstep  11618  prodmodclem2a  11760  fprod2dlemstep  11806  bitsfzo  12139  phimullem  12420  1arith  12563  ennnfonelemdm  12664  trivsubgsnd  13409  ssnmz  13419  trivnsgd  13425  kerf1ghm  13482  conjnmz  13487  unitssd  13743  subrguss  13870  unitrrg  13901  lsssssubg  14012  lssintclm  14018  zsssubrg  14219  mulgrhm2  14244  znrrg  14294  psrbaglesuppg  14306  bastg  14405  tgss  14407  tgtop  14412  tgidm  14418  neisspw  14492  topssnei  14506  tgrest  14513  ssrest  14526  cnss1  14570  cnss2  14571  cnsscnp  14573  cnrest2r  14581  txdis  14621  xblss2ps  14748  xblss2  14749  xmettxlem  14853  xmettx  14854  cncfss  14927  cnopnap  14955  dvfgg  15032  dvcj  15053