Theorem ssrdv 3233

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

Syntax hints:   → wi 4  ∀wal 1395   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqelssd  3246  sscon  3341  ssdif  3342  unss1  3376  ssrin  3432  eq0rdv  3539  uniss  3914  intss1  3943  intmin  3948  intssunim  3950  iunss1  3981  iinss1  3982  ss2iun  3985  ssiun  4012  ssiun2  4013  iinss  4022  iinss2  4023  exmidundif  4296  exmidundifim  4297  sspwb  4308  tron  4479  ssorduni  4585  ordsson  4590  ordpwsucss  4665  xpsspw  4838  relop  4880  dmss  4930  dmcosseq  5004  ssrnres  5179  chfnrn  5758  ffnfv  5805  f1imass  5915  fo1stresm  6324  fo2ndresm  6325  oprssdmm  6334  fo2ndf  6392  reldmtpos  6419  smoiun  6467  tfrlemi14d  6499  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemres  6528  dcdifsnid  6672  qsss  6763  pmss12g  6844  mapss  6860  ixpssmap2g  6896  ixpssmapg  6897  en2eqpr  7099  exmidpw  7100  exmidpweq  7101  onunsnss  7109  undifdcss  7115  ssfii  7173  fiss  7176  difinfsn  7299  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  ltprordil  7809  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  aptiprleml  7859  aptiprlemu  7860  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  suplocexprlemss  7935  suplocexprlemex  7942  peano5uzti  9588  uzss  9777  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iocssre  10188  icossre  10189  iccssre  10190  icodisj  10227  fzss1  10298  fzss2  10299  fzoss1  10408  fzosplit  10414  fzouzsplit  10416  ssfzo12bi  10471  frecuzrdgtcl  10675  frecuzrdgdomlem  10680  sswrd  11126  ovshftex  11397  summodclem2a  11960  fsum3cvg3  11975  fsum2dlemstep  12013  prodmodclem2a  12155  fprod2dlemstep  12201  bitsfzo  12534  phimullem  12815  1arith  12958  ennnfonelemdm  13059  trivsubgsnd  13806  ssnmz  13816  trivnsgd  13822  kerf1ghm  13879  conjnmz  13884  unitssd  14142  subrguss  14269  unitrrg  14300  lsssssubg  14411  lssintclm  14417  zsssubrg  14618  mulgrhm2  14643  znrrg  14693  psrbaglesuppg  14705  bastg  14804  tgss  14806  tgtop  14811  tgidm  14817  neisspw  14891  topssnei  14905  tgrest  14912  ssrest  14925  cnss1  14969  cnss2  14970  cnsscnp  14972  cnrest2r  14980  txdis  15020  xblss2ps  15147  xblss2  15148  xmettxlem  15252  xmettx  15253  cncfss  15326  cnopnap  15354  dvfgg  15431  dvcj  15452  usgruspgrben  16056  uhgrissubgr  16131  uhgrspansubgrlem  16146