Theorem ssrdv 3921

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 1934	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		df-ss 3900	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 235	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ss 3900

This theorem is referenced by:  eqelssd  3936  ss2abim  3991  ss2abdv  3996  sscon  4073  ssdif  4074  unss1  4114  ssrin  4170  eq0rdvALT  4336  sspw  4540  elpwdifsn  4722  uniss  4846  intss1  4893  intmin  4898  intssuni  4900  iinssiun  4935  iunss1  4936  iinss1  4937  ss2iun  4940  ssiun  4976  ssiun2  4977  iinss  4986  iinss2  4987  iunxdif3  5024  sspwb  5388  pwssun  5510  relop  5792  dmss  5844  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  imadifssran  6102  ssrnres  6129  sossfld  6137  predtrss  6273  preddowncl  6283  tron  6333  tz7.7  6336  funimassd  6893  dffv2  6922  chfnrn  6990  fvn0ssdmfun  7015  fveqdmss  7019  dff3  7041  ffnfv  7060  f1imass  7208  ssorduni  7722  onint  7733  limsssuc  7790  limuni3  7792  limomss  7811  fo1stres  7957  fo2ndres  7958  fo2ndf  8060  fnse  8073  ressuppssdif  8125  suppss  8134  reldmtpos  8174  fprlem2  8241  onfununi  8271  smoiun  8291  smocdmdom  8298  tz7.48-1  8372  tz7.49  8374  oaass  8486  cofon1  8598  cofon2  8599  qsss  8712  uniinqs  8734  pmss12g  8807  mapss  8827  ixpssmap2g  8865  ixpssmapg  8866  pssnn  9093  fineqv  9167  unifi3  9262  finnzfsuppd  9276  ssfii  9322  dffi2  9326  oismo  9445  unxpwdom2  9493  inf3lemd  9539  inf3lem1  9540  inf3lem6  9545  cantnflem3  9603  cantnf  9605  cnfcom3lem  9615  onssr1  9746  rankunb  9765  tcrank  9799  harcard  9893  carduni  9896  infxpenlem  9926  infpwfien  9975  dfac12r  10060  ackbij2lem1  10131  ackbij1lem18  10149  isfin1-3  10299  fin1a2lem11  10323  fin1a2lem13  10325  zorn2lem4  10412  zorn2lem5  10413  ttukeylem6  10427  ttukeylem7  10428  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2  10557  wunr1om  10633  wunom  10634  tskr1om  10681  tskr1om2  10682  tskxpss  10686  tskcard  10695  tskuni  10697  grothomex  10743  genpss  10918  distrlem1pr  10939  distrlem5pr  10941  ltexprlem2  10951  ltexprlem6  10955  ltexprlem7  10956  reclem3pr  10963  reclem4pr  10964  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  peano5uzi  12609  uzss  12802  ixxdisj  13304  ixxss1  13307  ixxss2  13308  ixxss12  13309  ixxub  13310  ixxlb  13311  iocssre  13371  icossre  13372  iccssre  13373  icodisj  13420  fzss1  13508  fzss2  13509  ssfzunsnext  13514  fzosplit  13638  fzouzsplit  13640  ssfzo12bi  13707  ssnn0fi  13938  fsuppmapnn0fiub  13944  suppssfz  13947  sswrd  14475  rtrclreclem3  15013  isercoll  15621  summolem2a  15668  fsumcvg3  15682  fsum2dlem  15723  fsumcom2  15727  qshash  15781  prodmolem2a  15890  fprod2dlem  15936  fprodcom2  15940  bitsfzo  16395  1arith  16889  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  ramtlecl  16962  prmgaplem3  17015  prmgaplem4  17016  monhom  17693  epihom  17700  funcsetcres2  18051  funcestrcsetclem8  18104  funcsetcestrclem8  18119  psdmrn  18530  chnrss  18572  chndss  18573  gsumwspan  18805  frmdss2  18822  sursubmefmnd  18855  injsubmefmnd  18856  trivsubgsnd  19120  ssnmz  19132  trivnsgd  19138  kerf1ghm  19213  conjnmz  19218  symgvalstruct  19363  gex1  19557  sylow2alem1  19583  lsmless1x  19610  lsmless2x  19611  lsmub1x  19612  lsmub2x  19613  lsmmod  19641  lsmdisj2  19648  efgrelexlemb  19716  efgcpbllemb  19721  cntzcmn  19806  gsum2d2  19940  dprdub  19993  dprdss  19997  dprddisj2  20007  pgpfac1lem3  20045  subrngmre  20534  subrguss  20559  subrgmre  20569  rnghmsscmap2  20601  rnghmsscmap  20602  funcrngcsetc  20612  funcrngcsetcALT  20613  rhmsscmap2  20630  rhmsscmap  20631  rhmsscrnghm  20637  rngcresringcat  20641  funcringcsetc  20646  unitrrg  20675  isdrng2  20715  primefld0cl  20778  primefld1cl  20779  lssssr  20944  lsssssubg  20948  lssmre  20956  lbspss  21072  lspdisj  21118  lbsextlem2  21152  lidl1el  21219  drngnidl  21236  lpiss  21322  zsssubrg  21400  qsssubdrg  21401  cnsubrg  21402  mulgrhm2  21453  znrrg  21540  ocvocv  21646  ocv2ss  21648  ocvin  21649  lsmcss  21667  cssmre  21668  pjcss  21691  lindfrn  21796  sraassab  21843  mhpsubg  22141  evls1maprnss  22364  dmatsgrp  22482  scmatsgrp  22502  scmatsgrp1  22505  m2cpmrngiso  22741  bastg  22949  tgss  22951  tgtop  22956  tgidm  22963  en2top  22968  neisspw  23090  topssnei  23107  neiptopuni  23113  lpss3  23127  clslp  23131  tgrest  23142  ssrest  23159  restntr  23165  ordtbas2  23174  ordtbas  23175  cnss1  23259  cnss2  23260  cnsscnp  23262  cnrest2r  23270  cmpsublem  23382  cmpsub  23383  tgcmp  23384  cmpcld  23385  hauscmplem  23389  cnconn  23405  llyss  23462  nllyss  23463  restnlly  23465  restlly  23466  locfincmp  23509  locfincf  23514  kgenss  23526  kgenidm  23530  llycmpkgen2  23533  1stckgen  23537  kgen2ss  23538  kgencn3  23541  ptbasfi  23564  ptpjopn  23595  txdis  23615  txkgen  23635  xkoptsub  23637  xkopjcn  23639  txconn  23672  qtoptop2  23682  qtopuni  23685  qtopkgen  23693  basqtop  23694  tgqtop  23695  qtopss  23698  qtoprest  23700  qtopomap  23701  qtopcmap  23702  kqsat  23714  kqcldsat  23716  hmphdis  23779  isfild  23841  ssfg  23855  fgss  23856  fgss2  23857  fgfil  23858  fgabs  23862  filconn  23866  fgtr  23873  uzrest  23880  ufilmax  23890  ufileu  23902  filufint  23903  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem4  23940  flimss2  23955  flimss1  23956  flimclsi  23961  flimcf  23965  flimsncls  23969  fclssscls  24001  fclsss1  24005  fclsss2  24006  fclscf  24008  uffclsflim  24014  alexsublem  24027  alexsubALTlem3  24032  ptcmplem2  24036  ptcmplem3  24037  cnextf  24049  efmndtmd  24084  symgtgp  24089  cldsubg  24094  tsmscl  24118  haustsms2  24120  tgptsmscls  24133  tsmsxp  24138  restutop  24220  ustuqtop4  24227  utop2nei  24233  utop3cls  24234  ucncn  24267  xblss2ps  24384  xblss2  24385  xrsblre  24795  xrsmopn  24796  recld2  24798  zdis  24800  icccmplem2  24807  cncfss  24884  cnheiborlem  24939  htpycn  24958  phtpyhtpy  24967  pi1blem  25024  cphsscph  25236  cfilfcls  25259  iscmet3lem2  25277  iscmet2  25279  caussi  25282  equivcfil  25284  lmcau  25298  metsscmetcld  25300  hlhil  25428  ivthicc  25443  ovoliunnul  25492  ovolicopnf  25509  uniioombllem3  25570  dyadmbllem  25584  volsup2  25590  vitalilem2  25594  itg1addlem4  25684  itg10a  25695  itg1ge0a  25696  mbfi1fseqlem4  25703  itg2gt0  25745  limciun  25879  perfdvf  25888  cpnord  25920  dvcj  25935  dvlip2  25980  dvivth  25995  dvne0  25996  dvcnvre  26004  ply1lpir  26165  plyco0  26175  plyexmo  26297  abelth  26424  efif1o  26528  logno1  26618  efopnlem2  26639  loglesqrt  26743  lgamcvg2  27036  ppisval  27085  ppinprm  27133  chtnprm  27135  fsumvma  27194  dchrfi  27236  chtppilimlem2  27455  chebbnd2  27458  vmadivsumb  27464  rplogsumlem2  27466  dchrisumlem2  27471  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selbergb  27530  selberg2b  27533  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrlog2bndlem2  27559  pntrlog2bndlem4  27561  oldssmade  27877  ltslpss  27918  noseqrdgfn  28316  n0ssoldg  28363  peano5uzs  28414  uhgredgss  29218  usgruspgrb  29270  uhgrissubgr  29362  uhgrspansubgrlem  29377  uhgrspan1  29390  cusgredg  29511  usgredgsscusgredg  29546  ococss  31382  shsub1  31413  shless  31448  shmodsi  31478  pjhth  31482  spansnss  31660  spanpr  31669  spansnm0i  31739  pjjsi  31789  sumdmdii  32504  sumdmdlem  32507  sumdmdlem2  32508  cdj3lem1  32523  abrexss  32600  fnpreimac  32762  rnmposs  32765  uzssico  32876  ssnnssfz  32879  pwrssmgc  33079  pmtrcnel  33170  cycpmrn  33224  cyc3evpm  33231  cycpmgcl  33234  elrgspnlem1  33323  elrgspnlem3  33325  elrgspnlem4  33326  elrgspnsubrunlem2  33329  fldgensdrg  33398  ringlsmss1  33479  ringlsmss2  33480  prmidlssidl  33528  mxidlirredi  33554  drngmxidl  33560  drngmxidlr  33561  1arithidomlem1  33618  1arithidom  33620  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  ply1mulrtss  33665  esplyfvaln  33758  dimkerim  33811  extdg1id  33850  irngss  33871  irngssv  33872  algextdeglem8  33908  constrsscn  33924  constrsslem  33925  constrsdrg  33959  crefss  34033  cmpcref  34034  zarmxt1  34064  tpr2rico  34096  esumrnmpt2  34252  esumpcvgval  34262  ldsysgenld  34344  sigapildsys  34346  ldgenpisys  34350  cldssbrsiga  34371  measdivcstALTV  34409  mbfmcnt  34452  oddpwdc  34538  eulerpartlemgs2  34564  reprpmtf1o  34810  bnj1033  35151  bnj1398  35216  trssfir1om  35292  r1omhfb  35293  trssfir1omregs  35317  r1omhfbregs  35318  sconnpi1  35467  cvmscld  35501  cvmliftlem15  35526  satfrnmapom  35598  dfon2lem6  36014  fnessref  36585  fgmin  36598  tailfb  36605  dissneqlem  37702  icoreresf  37714  rdglimss  37739  finxpreclem6  37758  lindsenlbs  37982  poimirlem11  37998  poimirlem12  37999  sstotbnd3  38143  prdstotbnd  38161  cntotbnd  38163  ismtyhmeo  38172  1idl  38393  disjdmqsss  39272  lshpdisj  39479  lssats  39504  lkrin  39656  glbconxN  39870  paddss1  40309  paddss2  40310  paddasslem16  40327  paddidm  40333  pmodlem2  40339  pmapjoin  40344  pmapjat1  40345  pclfinN  40392  pclfinclN  40442  diasslssN  41551  dia2dimlem12  41567  dihsslss  41768  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  zndvdchrrhm  42458  dvrelog2  42549  dvrelog3  42550  aks4d1p3  42563  aks4d1p4  42564  aks4d1p5  42565  aks4d1p7  42568  aks4d1p8  42572  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  hashscontpow1  42606  aks6d1c4  42609  sticksstones3  42633  aks6d1c6lem3  42657  aks6d1c6isolem2  42660  aks6d1c6lem5  42662  rhmqusspan  42670  unitscyglem1  42680  unitscyglem4  42683  eldiophss  43223  rencldnfilem  43265  pellexlem5  43278  pell14qrss1234  43301  pell1qrss14  43313  pellfundre  43326  pellfundge  43327  pellfundlb  43329  pellfundglb  43330  harinf  43479  proot1hash  43640  safesnsupfiss  43859  intabssd  43963  ss2iundf  44103  ov2ssiunov2  44144  clsk1indlem3  44487  radcnvrat  44758  nznngen  44760  trsspwALT3  45263  sspwimpALT2  45371  refsumcn  45478  iinssf  45585  icoiccdif  45969  icccncfext  46330  stoweidlem27  46470  stoweidlem46  46489  stoweidlem57  46500  fourierdlem40  46590  fourierdlem78  46627  ffnafv  47634  iccpartrn  47905  sprsymrelfvlem  47965  sprsymrelf1lem  47966  clnbgrssedg  48332  stgrusgra  48450  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem8  48788  funcringcsetclem8ALTV  48811  ssnn0ssfz  48840  lincolss  48925  lcoss  48927  lcosslsp  48929  iunord  50166