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  7441  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  ltprordil  7957  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  aptiprleml  8007  aptiprlemu  8008  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  suplocexprlemss  8083  suplocexprlemex  8090  peano5uzti  9759  uzss  9953  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iocssre  10366  icossre  10367  iccssre  10368  icodisj  10405  fzss1  10480  fzss2  10481  fzoss1  10591  fzosplit  10597  fzouzsplit  10599  ssfzo12bi  10654  frecuzrdgtcl  10864  frecuzrdgdomlem  10869  sswrd  11329  ovshftex  11600  summodclem2a  12167  fsum3cvg3  12182  fsum2dlemstep  12220  prodmodclem2a  12362  fprod2dlemstep  12408  bitsfzo  12741  phimullem  13026  1arith  13169  ennnfonelemdm  13363  trivsubgsnd  14057  ssnmz  14067  trivnsgd  14073  kerf1ghm  14130  conjnmz  14135  unitssd  14500  subrguss  14628  unitrrg  14660  lsssssubg  14799  lssintclm  14805  zsssubrg  15006  mulgrhm2  15029  znrrg  15079  psrbaglesuppg  15141  psrbaglefifi  15147  bastg  15253  tgss  15255  tgtop  15260  tgidm  15266  neisspw  15340  topssnei  15354  tgrest  15361  ssrest  15374  cnss1  15418  cnss2  15419  cnsscnp  15421  cnrest2r  15429  txdis  15469  xblss2ps  15596  xblss2  15597  xmettxlem  15701  xmettx  15702  cncfss  15775  cnopnap  15803  dvfgg  15880  dvcj  15901  ppiqsval  16201  ppinprm  16221  chtnprm  16223  usgruspgrben  16593  uhgrissubgr  16668  uhgrspansubgrlem  16683