Theorem ssrdv 3203

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

Syntax hints:   → wi 4  ∀wal 1371   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqelssd  3216  sscon  3311  ssdif  3312  unss1  3346  ssrin  3402  eq0rdv  3509  uniss  3876  intss1  3905  intmin  3910  intssunim  3912  iunss1  3943  iinss1  3944  ss2iun  3947  ssiun  3974  ssiun2  3975  iinss  3984  iinss2  3985  exmidundif  4257  exmidundifim  4258  sspwb  4267  tron  4436  ssorduni  4542  ordsson  4547  ordpwsucss  4622  xpsspw  4794  relop  4835  dmss  4885  dmcosseq  4958  ssrnres  5133  chfnrn  5703  ffnfv  5750  f1imass  5855  fo1stresm  6259  fo2ndresm  6260  oprssdmm  6269  fo2ndf  6325  reldmtpos  6351  smoiun  6399  tfrlemi14d  6431  tfr1onlemres  6447  tfri1dALT  6449  tfrcllemres  6460  dcdifsnid  6602  qsss  6693  pmss12g  6774  mapss  6790  ixpssmap2g  6826  ixpssmapg  6827  en2eqpr  7018  exmidpw  7019  exmidpweq  7020  onunsnss  7028  undifdcss  7034  ssfii  7090  fiss  7093  difinfsn  7216  addnqprlemrl  7685  addnqprlemru  7686  addnqprlemfl  7687  addnqprlemfu  7688  mulnqprlemrl  7701  mulnqprlemru  7702  mulnqprlemfl  7703  mulnqprlemfu  7704  distrlem1prl  7710  distrlem1pru  7711  distrlem5prl  7714  distrlem5pru  7715  ltprordil  7717  ltexprlemfl  7737  ltexprlemrl  7738  ltexprlemfu  7739  ltexprlemru  7740  addcanprleml  7742  addcanprlemu  7743  recexprlem1ssl  7761  recexprlem1ssu  7762  recexprlemss1l  7763  recexprlemss1u  7764  aptiprleml  7767  aptiprlemu  7768  cauappcvgprlemladdfu  7782  cauappcvgprlemladdfl  7783  cauappcvgprlemladdru  7784  cauappcvgprlemladdrl  7785  caucvgprlemladdfu  7805  caucvgprlemladdrl  7806  suplocexprlemss  7843  suplocexprlemex  7850  peano5uzti  9496  uzss  9684  ixxdisj  10040  ixxss1  10041  ixxss2  10042  ixxss12  10043  iocssre  10090  icossre  10091  iccssre  10092  icodisj  10129  fzss1  10200  fzss2  10201  fzoss1  10310  fzosplit  10316  fzouzsplit  10318  ssfzo12bi  10371  frecuzrdgtcl  10574  frecuzrdgdomlem  10579  sswrd  11020  ovshftex  11200  summodclem2a  11762  fsum3cvg3  11777  fsum2dlemstep  11815  prodmodclem2a  11957  fprod2dlemstep  12003  bitsfzo  12336  phimullem  12617  1arith  12760  ennnfonelemdm  12861  trivsubgsnd  13607  ssnmz  13617  trivnsgd  13623  kerf1ghm  13680  conjnmz  13685  unitssd  13941  subrguss  14068  unitrrg  14099  lsssssubg  14210  lssintclm  14216  zsssubrg  14417  mulgrhm2  14442  znrrg  14492  psrbaglesuppg  14504  bastg  14603  tgss  14605  tgtop  14610  tgidm  14616  neisspw  14690  topssnei  14704  tgrest  14711  ssrest  14724  cnss1  14768  cnss2  14769  cnsscnp  14771  cnrest2r  14779  txdis  14819  xblss2ps  14946  xblss2  14947  xmettxlem  15051  xmettx  15052  cncfss  15125  cnopnap  15153  dvfgg  15230  dvcj  15251