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 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   ∈ wcel 2209   ⊆ wss 3220

This proof depends on 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 proof 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 used by:  eqelssd  3267  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  eq0rdv  3571  sspw  3702  uniss  3956  intss1  3985  intmin  3990  intssunim  3992  iunss1  4023  iinss1  4024  ss2iun  4027  ssiun  4054  ssiun2  4055  iinss  4064  iinss2  4065  exmidundif  4343  exmidundifim  4344  sspwb  4356  tron  4527  ssorduni  4634  ordsson  4639  ordpwsucss  4714  xpsspw  4887  relop  4930  dmss  4980  dmcosseq  5054  ssrnres  5230  chfnrn  5820  ffnfv  5866  f1imass  5980  abrexss  6358  fo1stresm  6395  fo2ndresm  6396  oprssdmm  6405  fo2ndf  6463  funsssuppss  6498  suppssdc  6500  suppssfvg  6503  reldmtpos  6524  smoiun  6572  tfrlemi14d  6604  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemres  6633  dcdifsnid  6777  qsss  6868  pmss12g  6956  mapss  6973  ixpssmap2g  7009  ixpssmapg  7010  en2eqpr  7214  exmidpw  7215  exmidpweq  7216  onunsnss  7224  undifdcss  7230  ssfii  7308  fiss  7311  difinfsn  7440  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  ltprordil  7956  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  suplocexprlemss  8082  suplocexprlemex  8089  peano5uzti  9754  uzss  9943  ixxdisj  10305  ixxss1  10306  ixxss2  10307  ixxss12  10308  iocssre  10355  icossre  10356  iccssre  10357  icodisj  10394  fzss1  10469  fzss2  10470  fzoss1  10580  fzosplit  10586  fzouzsplit  10588  ssfzo12bi  10643  frecuzrdgtcl  10849  frecuzrdgdomlem  10854  sswrd  11313  ovshftex  11584  summodclem2a  12148  fsum3cvg3  12163  fsum2dlemstep  12201  prodmodclem2a  12343  fprod2dlemstep  12389  bitsfzo  12722  phimullem  13003  1arith  13146  ennnfonelemdm  13311  trivsubgsnd  14004  ssnmz  14014  trivnsgd  14020  kerf1ghm  14077  conjnmz  14082  unitssd  14416  subrguss  14544  unitrrg  14576  lsssssubg  14715  lssintclm  14721  zsssubrg  14922  mulgrhm2  14945  znrrg  14995  psrbaglesuppg  15057  bastg  15162  tgss  15164  tgtop  15169  tgidm  15175  neisspw  15249  topssnei  15263  tgrest  15270  ssrest  15283  cnss1  15327  cnss2  15328  cnsscnp  15330  cnrest2r  15338  txdis  15378  xblss2ps  15505  xblss2  15506  xmettxlem  15610  xmettx  15611  cncfss  15684  cnopnap  15712  dvfgg  15789  dvcj  15810  usgruspgrben  16427  uhgrissubgr  16502  uhgrspansubgrlem  16517