Theorem ssrdv 3230

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

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

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 3203  df-ss 3210

This theorem is referenced by:  eqelssd  3243  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  eq0rdv  3536  uniss  3908  intss1  3937  intmin  3942  intssunim  3944  iunss1  3975  iinss1  3976  ss2iun  3979  ssiun  4006  ssiun2  4007  iinss  4016  iinss2  4017  exmidundif  4289  exmidundifim  4290  sspwb  4301  tron  4472  ssorduni  4578  ordsson  4583  ordpwsucss  4658  xpsspw  4830  relop  4871  dmss  4921  dmcosseq  4995  ssrnres  5170  chfnrn  5745  ffnfv  5792  f1imass  5897  fo1stresm  6305  fo2ndresm  6306  oprssdmm  6315  fo2ndf  6371  reldmtpos  6397  smoiun  6445  tfrlemi14d  6477  tfr1onlemres  6493  tfri1dALT  6495  tfrcllemres  6506  dcdifsnid  6648  qsss  6739  pmss12g  6820  mapss  6836  ixpssmap2g  6872  ixpssmapg  6873  en2eqpr  7065  exmidpw  7066  exmidpweq  7067  onunsnss  7075  undifdcss  7081  ssfii  7137  fiss  7140  difinfsn  7263  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  distrlem1prl  7765  distrlem1pru  7766  distrlem5prl  7769  distrlem5pru  7770  ltprordil  7772  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  aptiprleml  7822  aptiprlemu  7823  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  suplocexprlemss  7898  suplocexprlemex  7905  peano5uzti  9551  uzss  9739  ixxdisj  10095  ixxss1  10096  ixxss2  10097  ixxss12  10098  iocssre  10145  icossre  10146  iccssre  10147  icodisj  10184  fzss1  10255  fzss2  10256  fzoss1  10365  fzosplit  10371  fzouzsplit  10373  ssfzo12bi  10426  frecuzrdgtcl  10629  frecuzrdgdomlem  10634  sswrd  11075  ovshftex  11325  summodclem2a  11887  fsum3cvg3  11902  fsum2dlemstep  11940  prodmodclem2a  12082  fprod2dlemstep  12128  bitsfzo  12461  phimullem  12742  1arith  12885  ennnfonelemdm  12986  trivsubgsnd  13733  ssnmz  13743  trivnsgd  13749  kerf1ghm  13806  conjnmz  13811  unitssd  14067  subrguss  14194  unitrrg  14225  lsssssubg  14336  lssintclm  14342  zsssubrg  14543  mulgrhm2  14568  znrrg  14618  psrbaglesuppg  14630  bastg  14729  tgss  14731  tgtop  14736  tgidm  14742  neisspw  14816  topssnei  14830  tgrest  14837  ssrest  14850  cnss1  14894  cnss2  14895  cnsscnp  14897  cnrest2r  14905  txdis  14945  xblss2ps  15072  xblss2  15073  xmettxlem  15177  xmettx  15178  cncfss  15251  cnopnap  15279  dvfgg  15356  dvcj  15377  usgruspgrben  15978