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  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  distrlem1prl  6558  distrlem1pru  6559  distrlem5prl  6562  distrlem5pru  6563  ltprordil  6565  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  aptiprleml  6611  aptiprlemu  6612  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  peano5uzti  8122  uzss  8269  ixxdisj  8542  ixxss1  8543  ixxss2  8544  ixxss12  8545  iocssre  8592  icossre  8593  iccssre  8594  icodisj  8630  fzss1  8696  fzss2  8697  fzoss1  8797  fzosplit  8803  fzouzsplit  8805  ssfzo12bi  8851  frecuzrdgfn  8879