Theorem ssrdv 3103

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

Syntax hints:   → wi 4  ∀wal 1329   ∈ wcel 1480   ⊆ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  eqelssd  3116  sscon  3210  ssdif  3211  unss1  3245  ssrin  3301  eq0rdv  3407  uniss  3757  intss1  3786  intmin  3791  intssunim  3793  iunss1  3824  iinss1  3825  ss2iun  3828  ssiun  3855  ssiun2  3856  iinss  3864  iinss2  3865  exmidundif  4129  exmidundifim  4130  sspwb  4138  tron  4304  ssorduni  4403  ordsson  4408  ordpwsucss  4482  xpsspw  4651  relop  4689  dmss  4738  dmcosseq  4810  ssrnres  4981  chfnrn  5531  ffnfv  5578  f1imass  5675  fo1stresm  6059  fo2ndresm  6060  oprssdmm  6069  fo2ndf  6124  reldmtpos  6150  smoiun  6198  tfrlemi14d  6230  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemres  6259  dcdifsnid  6400  qsss  6488  pmss12g  6569  mapss  6585  ixpssmap2g  6621  ixpssmapg  6622  en2eqpr  6801  exmidpw  6802  onunsnss  6805  undifdcss  6811  ssfii  6862  fiss  6865  difinfsn  6985  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  distrlem1prl  7390  distrlem1pru  7391  distrlem5prl  7394  distrlem5pru  7395  ltprordil  7397  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  aptiprleml  7447  aptiprlemu  7448  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  suplocexprlemss  7523  suplocexprlemex  7530  peano5uzti  9159  uzss  9346  ixxdisj  9686  ixxss1  9687  ixxss2  9688  ixxss12  9689  iocssre  9736  icossre  9737  iccssre  9738  icodisj  9775  fzss1  9843  fzss2  9844  fzoss1  9948  fzosplit  9954  fzouzsplit  9956  ssfzo12bi  10002  frecuzrdgtcl  10185  frecuzrdgdomlem  10190  ovshftex  10591  summodclem2a  11150  fsum3cvg3  11165  fsum2dlemstep  11203  prodmodclem2a  11345  phimullem  11901  ennnfonelemdm  11933  bastg  12230  tgss  12232  tgtop  12237  tgidm  12243  neisspw  12317  topssnei  12331  tgrest  12338  ssrest  12351  cnss1  12395  cnss2  12396  cnsscnp  12398  cnrest2r  12406  txdis  12446  xblss2ps  12573  xblss2  12574  xmettxlem  12678  xmettx  12679  cncfss  12739  cnopnap  12763  dvfgg  12826  dvcj  12842