Theorem ssrdv 2945

Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
ssrdv.1	⊢ (φ → (x ∈ A → x ∈ B))

Assertion

Ref	Expression
ssrdv	⊢ (φ → A ⊆ B)

Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (φ → (x ∈ A → x ∈ B))
2	1	alrimiv 1751	. 2 ⊢ (φ → ∀x(x ∈ A → x ∈ B))
3		dfss2 2928	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4	2, 3	sylibr 137	1 ⊢ (φ → A ⊆ B)

Syntax hints:   → wi 4  ∀wal 1240   ∈ wcel 1390   ⊆ wss 2911

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925

This theorem is referenced by:  sscon  3071  ssdif  3072  unss1  3106  ssrin  3156  eq0rdv  3255  uniss  3592  intss1  3621  intmin  3626  intssunim  3628  iunss1  3659  iinss1  3660  ss2iun  3663  ssiun  3690  ssiun2  3691  iinss  3699  iinss2  3700  trintssm  3861  sspwb  3943  tron  4085  ssorduni  4179  ordsson  4184  ordpwsucss  4243  xpsspw  4393  relop  4429  dmss  4477  dmcosseq  4546  ssrnres  4706  chfnrn  5221  ffnfv  5266  f1imass  5356  fo1stresm  5730  fo2ndresm  5731  fo2ndf  5790  reldmtpos  5809  smoiun  5857  tfrlemi14d  5888  qsss  6101  addnqprlemrl  6537  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  distrlem1prl  6557  distrlem1pru  6558  distrlem5prl  6561  distrlem5pru  6562  ltprordil  6564  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  aptiprleml  6610  aptiprlemu  6611  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  peano5uzti  8102  uzss  8249  ixxdisj  8522  ixxss1  8523  ixxss2  8524  ixxss12  8525  iocssre  8572  icossre  8573  iccssre  8574  icodisj  8610  fzss1  8676  fzss2  8677  fzoss1  8777  fzosplit  8783  fzouzsplit  8785  ssfzo12bi  8831  frecuzrdgfn  8859