Theorem ssrdv 3233

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

Syntax hints:   → wi 4  ∀wal 1395   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqelssd  3246  sscon  3341  ssdif  3342  unss1  3376  ssrin  3432  eq0rdv  3539  uniss  3914  intss1  3943  intmin  3948  intssunim  3950  iunss1  3981  iinss1  3982  ss2iun  3985  ssiun  4012  ssiun2  4013  iinss  4022  iinss2  4023  exmidundif  4296  exmidundifim  4297  sspwb  4308  tron  4479  ssorduni  4585  ordsson  4590  ordpwsucss  4665  xpsspw  4838  relop  4880  dmss  4930  dmcosseq  5004  ssrnres  5179  chfnrn  5758  ffnfv  5805  f1imass  5914  fo1stresm  6323  fo2ndresm  6324  oprssdmm  6333  fo2ndf  6391  reldmtpos  6418  smoiun  6466  tfrlemi14d  6498  tfr1onlemres  6514  tfri1dALT  6516  tfrcllemres  6527  dcdifsnid  6671  qsss  6762  pmss12g  6843  mapss  6859  ixpssmap2g  6895  ixpssmapg  6896  en2eqpr  7098  exmidpw  7099  exmidpweq  7100  onunsnss  7108  undifdcss  7114  ssfii  7172  fiss  7175  difinfsn  7298  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  distrlem1prl  7801  distrlem1pru  7802  distrlem5prl  7805  distrlem5pru  7806  ltprordil  7808  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  aptiprleml  7858  aptiprlemu  7859  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  suplocexprlemss  7934  suplocexprlemex  7941  peano5uzti  9587  uzss  9776  ixxdisj  10137  ixxss1  10138  ixxss2  10139  ixxss12  10140  iocssre  10187  icossre  10188  iccssre  10189  icodisj  10226  fzss1  10297  fzss2  10298  fzoss1  10407  fzosplit  10413  fzouzsplit  10415  ssfzo12bi  10469  frecuzrdgtcl  10673  frecuzrdgdomlem  10678  sswrd  11121  ovshftex  11379  summodclem2a  11941  fsum3cvg3  11956  fsum2dlemstep  11994  prodmodclem2a  12136  fprod2dlemstep  12182  bitsfzo  12515  phimullem  12796  1arith  12939  ennnfonelemdm  13040  trivsubgsnd  13787  ssnmz  13797  trivnsgd  13803  kerf1ghm  13860  conjnmz  13865  unitssd  14122  subrguss  14249  unitrrg  14280  lsssssubg  14391  lssintclm  14397  zsssubrg  14598  mulgrhm2  14623  znrrg  14673  psrbaglesuppg  14685  bastg  14784  tgss  14786  tgtop  14791  tgidm  14797  neisspw  14871  topssnei  14885  tgrest  14892  ssrest  14905  cnss1  14949  cnss2  14950  cnsscnp  14952  cnrest2r  14960  txdis  15000  xblss2ps  15127  xblss2  15128  xmettxlem  15232  xmettx  15233  cncfss  15306  cnopnap  15334  dvfgg  15411  dvcj  15432  usgruspgrben  16036  uhgrissubgr  16111  uhgrspansubgrlem  16126