Theorem ssrdv 3230

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

Syntax hints:   → wi 4  ∀wal 1393   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqelssd  3243  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  eq0rdv  3536  uniss  3909  intss1  3938  intmin  3943  intssunim  3945  iunss1  3976  iinss1  3977  ss2iun  3980  ssiun  4007  ssiun2  4008  iinss  4017  iinss2  4018  exmidundif  4290  exmidundifim  4291  sspwb  4302  tron  4473  ssorduni  4579  ordsson  4584  ordpwsucss  4659  xpsspw  4831  relop  4872  dmss  4922  dmcosseq  4996  ssrnres  5171  chfnrn  5748  ffnfv  5795  f1imass  5904  fo1stresm  6313  fo2ndresm  6314  oprssdmm  6323  fo2ndf  6379  reldmtpos  6405  smoiun  6453  tfrlemi14d  6485  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemres  6514  dcdifsnid  6658  qsss  6749  pmss12g  6830  mapss  6846  ixpssmap2g  6882  ixpssmapg  6883  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  onunsnss  7090  undifdcss  7096  ssfii  7152  fiss  7155  difinfsn  7278  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  ltprordil  7787  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  aptiprleml  7837  aptiprlemu  7838  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  suplocexprlemss  7913  suplocexprlemex  7920  peano5uzti  9566  uzss  9755  ixxdisj  10111  ixxss1  10112  ixxss2  10113  ixxss12  10114  iocssre  10161  icossre  10162  iccssre  10163  icodisj  10200  fzss1  10271  fzss2  10272  fzoss1  10381  fzosplit  10387  fzouzsplit  10389  ssfzo12bi  10443  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  sswrd  11093  ovshftex  11345  summodclem2a  11907  fsum3cvg3  11922  fsum2dlemstep  11960  prodmodclem2a  12102  fprod2dlemstep  12148  bitsfzo  12481  phimullem  12762  1arith  12905  ennnfonelemdm  13006  trivsubgsnd  13753  ssnmz  13763  trivnsgd  13769  kerf1ghm  13826  conjnmz  13831  unitssd  14088  subrguss  14215  unitrrg  14246  lsssssubg  14357  lssintclm  14363  zsssubrg  14564  mulgrhm2  14589  znrrg  14639  psrbaglesuppg  14651  bastg  14750  tgss  14752  tgtop  14757  tgidm  14763  neisspw  14837  topssnei  14851  tgrest  14858  ssrest  14871  cnss1  14915  cnss2  14916  cnsscnp  14918  cnrest2r  14926  txdis  14966  xblss2ps  15093  xblss2  15094  xmettxlem  15198  xmettx  15199  cncfss  15272  cnopnap  15300  dvfgg  15377  dvcj  15398  usgruspgrben  15999