Theorem ssrdv 3234

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

Syntax hints:   → wi 4  ∀wal 1396   ∈ wcel 2202   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqelssd  3247  sscon  3343  ssdif  3344  unss1  3378  ssrin  3434  eq0rdv  3541  uniss  3919  intss1  3948  intmin  3953  intssunim  3955  iunss1  3986  iinss1  3987  ss2iun  3990  ssiun  4017  ssiun2  4018  iinss  4027  iinss2  4028  exmidundif  4302  exmidundifim  4303  sspwb  4314  tron  4485  ssorduni  4591  ordsson  4596  ordpwsucss  4671  xpsspw  4844  relop  4886  dmss  4936  dmcosseq  5010  ssrnres  5186  chfnrn  5767  ffnfv  5813  f1imass  5925  fo1stresm  6333  fo2ndresm  6334  oprssdmm  6343  fo2ndf  6401  funsssuppss  6436  suppssdc  6438  suppssfvg  6441  reldmtpos  6462  smoiun  6510  tfrlemi14d  6542  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemres  6571  dcdifsnid  6715  qsss  6806  pmss12g  6887  mapss  6903  ixpssmap2g  6939  ixpssmapg  6940  en2eqpr  7142  exmidpw  7143  exmidpweq  7144  onunsnss  7152  undifdcss  7158  ssfii  7216  fiss  7219  difinfsn  7342  addnqprlemrl  7820  addnqprlemru  7821  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemrl  7836  mulnqprlemru  7837  mulnqprlemfl  7838  mulnqprlemfu  7839  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  ltprordil  7852  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  aptiprleml  7902  aptiprlemu  7903  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  suplocexprlemss  7978  suplocexprlemex  7985  peano5uzti  9632  uzss  9821  ixxdisj  10182  ixxss1  10183  ixxss2  10184  ixxss12  10185  iocssre  10232  icossre  10233  iccssre  10234  icodisj  10271  fzss1  10343  fzss2  10344  fzoss1  10453  fzosplit  10459  fzouzsplit  10461  ssfzo12bi  10516  frecuzrdgtcl  10720  frecuzrdgdomlem  10725  sswrd  11171  ovshftex  11442  summodclem2a  12005  fsum3cvg3  12020  fsum2dlemstep  12058  prodmodclem2a  12200  fprod2dlemstep  12246  bitsfzo  12579  phimullem  12860  1arith  13003  ennnfonelemdm  13104  trivsubgsnd  13851  ssnmz  13861  trivnsgd  13867  kerf1ghm  13924  conjnmz  13929  unitssd  14187  subrguss  14314  unitrrg  14346  lsssssubg  14457  lssintclm  14463  zsssubrg  14664  mulgrhm2  14689  znrrg  14739  psrbaglesuppg  14751  bastg  14855  tgss  14857  tgtop  14862  tgidm  14868  neisspw  14942  topssnei  14956  tgrest  14963  ssrest  14976  cnss1  15020  cnss2  15021  cnsscnp  15023  cnrest2r  15031  txdis  15071  xblss2ps  15198  xblss2  15199  xmettxlem  15303  xmettx  15304  cncfss  15377  cnopnap  15405  dvfgg  15482  dvcj  15503  usgruspgrben  16110  uhgrissubgr  16185  uhgrspansubgrlem  16200