Theorem ssrdv 3254

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

Syntax hints:   → wi 4  ∀wal 1400   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqelssd  3267  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  eq0rdv  3570  sspw  3698  uniss  3951  intss1  3980  intmin  3985  intssunim  3987  iunss1  4018  iinss1  4019  ss2iun  4022  ssiun  4049  ssiun2  4050  iinss  4059  iinss2  4060  exmidundif  4338  exmidundifim  4339  sspwb  4351  tron  4522  ssorduni  4629  ordsson  4634  ordpwsucss  4709  xpsspw  4882  relop  4925  dmss  4975  dmcosseq  5049  ssrnres  5225  chfnrn  5811  ffnfv  5857  f1imass  5970  abrexss  6348  fo1stresm  6385  fo2ndresm  6386  oprssdmm  6395  fo2ndf  6453  funsssuppss  6488  suppssdc  6490  suppssfvg  6493  reldmtpos  6514  smoiun  6562  tfrlemi14d  6594  tfr1onlemres  6610  tfri1dALT  6612  tfrcllemres  6623  dcdifsnid  6767  qsss  6858  pmss12g  6946  mapss  6963  ixpssmap2g  6999  ixpssmapg  7000  en2eqpr  7204  exmidpw  7205  exmidpweq  7206  onunsnss  7214  undifdcss  7220  ssfii  7298  fiss  7301  difinfsn  7430  addnqprlemrl  7914  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemrl  7930  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  ltprordil  7946  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  aptiprleml  7996  aptiprlemu  7997  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  suplocexprlemss  8072  suplocexprlemex  8079  peano5uzti  9733  uzss  9922  ixxdisj  10284  ixxss1  10285  ixxss2  10286  ixxss12  10287  iocssre  10334  icossre  10335  iccssre  10336  icodisj  10373  fzss1  10447  fzss2  10448  fzoss1  10558  fzosplit  10564  fzouzsplit  10566  ssfzo12bi  10621  frecuzrdgtcl  10827  frecuzrdgdomlem  10832  sswrd  11291  ovshftex  11562  summodclem2a  12126  fsum3cvg3  12141  fsum2dlemstep  12179  prodmodclem2a  12321  fprod2dlemstep  12367  bitsfzo  12700  phimullem  12981  1arith  13124  ennnfonelemdm  13289  trivsubgsnd  13981  ssnmz  13991  trivnsgd  13997  kerf1ghm  14054  conjnmz  14059  unitssd  14389  subrguss  14517  unitrrg  14549  lsssssubg  14687  lssintclm  14693  zsssubrg  14894  mulgrhm2  14917  znrrg  14967  psrbaglesuppg  14980  bastg  15085  tgss  15087  tgtop  15092  tgidm  15098  neisspw  15172  topssnei  15186  tgrest  15193  ssrest  15206  cnss1  15250  cnss2  15251  cnsscnp  15253  cnrest2r  15261  txdis  15301  xblss2ps  15428  xblss2  15429  xmettxlem  15533  xmettx  15534  cncfss  15607  cnopnap  15635  dvfgg  15712  dvcj  15733  usgruspgrben  16341  uhgrissubgr  16416  uhgrspansubgrlem  16431