Theorem ssrdv 3928

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  eqelssd  3943  ss2abdvALT  3999  sscon  4074  ssdif  4075  unss1  4114  ssrin  4168  eq0rdvALT  4340  sspw  4547  elpwdifsn  4723  uniss  4848  intss1  4895  intmin  4900  intssuni  4902  iinssiun  4938  iunss1  4939  iinss1  4940  ss2iun  4943  ssiun  4977  ssiun2  4978  iinss  4987  iinss2  4988  iunxdif3  5025  sspwb  5366  pwssun  5486  relop  5762  dmss  5814  dmcosseq  5885  ssrnres  6086  sossfld  6094  predtrss  6229  preddowncl  6239  tron  6293  tz7.7  6296  dffv2  6872  chfnrn  6935  fvn0ssdmfun  6961  fveqdmss  6965  dff3  6985  ffnfv  7001  f1imass  7146  ssorduni  7638  onint  7649  limsssuc  7706  limuni3  7708  limomss  7726  fo1stres  7866  fo2ndres  7867  fo2ndf  7971  fnse  7983  ressuppssdif  8010  suppss  8019  suppssOLD  8020  reldmtpos  8059  fprlem2  8126  onfununi  8181  smoiun  8201  smorndom  8208  tz7.48-1  8283  tz7.49  8285  oaass  8401  qsss  8576  uniinqs  8595  pmss12g  8666  mapss  8686  ixpssmap2g  8724  ixpssmapg  8725  pssnn  8960  fineqv  9047  pssnnOLD  9049  ssfii  9187  dffi2  9191  oismo  9308  unxpwdom2  9356  inf3lemd  9394  inf3lem1  9395  inf3lem6  9400  cantnflem3  9458  cantnf  9460  cnfcom3lem  9470  onssr1  9598  rankunb  9617  tcrank  9651  harcard  9745  carduni  9748  infxpenlem  9778  infpwfien  9827  dfac12r  9911  ackbij2lem1  9984  ackbij1lem18  10002  isfin1-3  10151  fin1a2lem11  10175  fin1a2lem13  10177  zorn2lem4  10264  zorn2lem5  10265  ttukeylem6  10279  ttukeylem7  10280  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2  10408  wunr1om  10484  wunom  10485  tskr1om  10532  tskr1om2  10533  tskxpss  10537  tskcard  10546  tskuni  10548  grothomex  10594  genpss  10769  distrlem1pr  10790  distrlem5pr  10792  ltexprlem2  10802  ltexprlem6  10806  ltexprlem7  10807  reclem3pr  10814  reclem4pr  10815  supaddc  11951  supadd  11952  supmul1  11953  supmullem2  11955  peano5uzi  12418  uzss  12614  ixxdisj  13103  ixxss1  13106  ixxss2  13107  ixxss12  13108  ixxub  13109  ixxlb  13110  iocssre  13168  icossre  13169  iccssre  13170  icodisj  13217  fzss1  13304  fzss2  13305  ssfzunsnext  13310  fzosplit  13429  fzouzsplit  13431  ssfzo12bi  13491  ssnn0fi  13714  fsuppmapnn0fiub  13720  suppssfz  13723  sswrd  14234  rtrclreclem3  14780  isercoll  15388  summolem2a  15436  fsumcvg3  15450  fsum2dlem  15491  fsumcom2  15495  qshash  15548  prodmolem2a  15653  fprod2dlem  15699  fprodcom2  15703  bitsfzo  16151  1arith  16637  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  ramtlecl  16710  prmgaplem3  16763  prmgaplem4  16764  monhom  17456  epihom  17463  funcsetcres2  17817  funcestrcsetclem8  17873  funcsetcestrclem8  17888  psdmrn  18300  gsumwspan  18494  frmdss2  18511  sursubmefmnd  18544  injsubmefmnd  18545  trivsubgsnd  18791  ssnmz  18803  trivnsgd  18809  conjnmz  18877  symgvalstruct  19013  symgvalstructOLD  19014  gex1  19205  sylow2alem1  19231  lsmless1x  19258  lsmless2x  19259  lsmub1x  19260  lsmub2x  19261  lsmmod  19290  lsmdisj2  19297  efgrelexlemb  19365  efgcpbllemb  19370  cntzcmn  19450  gsum2d2  19584  dprdub  19637  dprdss  19641  dprddisj2  19651  pgpfac1lem3  19689  kerf1ghm  19996  isdrng2  20010  subrguss  20048  subrgmre  20057  primefld0cl  20083  primefld1cl  20084  lssssr  20224  lsssssubg  20229  lssmre  20237  lbspss  20353  lspdisj  20396  lbsextlem2  20430  lidl1el  20498  drngnidl  20509  lpiss  20530  unitrrg  20573  zsssubrg  20665  qsssubdrg  20666  cnsubrg  20667  mulgrhm2  20709  znrrg  20782  ocvocv  20885  ocv2ss  20887  ocvin  20888  lsmcss  20906  cssmre  20907  pjcss  20932  lindfrn  21037  mhpsubg  21352  dmatsgrp  21657  scmatsgrp  21677  scmatsgrp1  21680  m2cpmrngiso  21916  bastg  22125  tgss  22127  tgtop  22132  tgidm  22139  en2top  22144  neisspw  22267  topssnei  22284  neiptopuni  22290  lpss3  22304  clslp  22308  tgrest  22319  ssrest  22336  restntr  22342  ordtbas2  22351  ordtbas  22352  cnss1  22436  cnss2  22437  cnsscnp  22439  cnrest2r  22447  cmpsublem  22559  cmpsub  22560  tgcmp  22561  cmpcld  22562  hauscmplem  22566  cnconn  22582  llyss  22639  nllyss  22640  restnlly  22642  restlly  22643  locfincmp  22686  locfincf  22691  kgenss  22703  kgenidm  22707  llycmpkgen2  22710  1stckgen  22714  kgen2ss  22715  kgencn3  22718  ptbasfi  22741  ptpjopn  22772  txdis  22792  txkgen  22812  xkoptsub  22814  xkopjcn  22816  txconn  22849  qtoptop2  22859  qtopuni  22862  qtopkgen  22870  basqtop  22871  tgqtop  22872  qtopss  22875  qtoprest  22877  qtopomap  22878  qtopcmap  22879  kqsat  22891  kqcldsat  22893  hmphdis  22956  isfild  23018  ssfg  23032  fgss  23033  fgss2  23034  fgfil  23035  fgabs  23039  filconn  23043  fgtr  23050  uzrest  23057  ufilmax  23067  ufileu  23079  filufint  23080  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem4  23117  flimss2  23132  flimss1  23133  flimclsi  23138  flimcf  23142  flimsncls  23146  fclssscls  23178  fclsss1  23182  fclsss2  23183  fclscf  23185  uffclsflim  23191  alexsublem  23204  alexsubALTlem3  23209  ptcmplem2  23213  ptcmplem3  23214  cnextf  23226  efmndtmd  23261  symgtgp  23266  cldsubg  23271  tsmscl  23295  haustsms2  23297  tgptsmscls  23310  tsmsxp  23315  restutop  23398  ustuqtop4  23405  utop2nei  23411  utop3cls  23412  ucncn  23446  xblss2ps  23563  xblss2  23564  xrsblre  23983  xrsmopn  23984  recld2  23986  zdis  23988  icccmplem2  23995  cncfss  24071  cnheiborlem  24126  htpycn  24145  phtpyhtpy  24154  pi1blem  24211  cphsscph  24424  cfilfcls  24447  iscmet3lem2  24465  iscmet2  24467  caussi  24470  equivcfil  24472  lmcau  24486  metsscmetcld  24488  hlhil  24616  ivthicc  24631  ovoliunnul  24680  ovolicopnf  24697  uniioombllem3  24758  dyadmbllem  24772  volsup2  24778  vitalilem2  24782  itg1addlem4  24872  itg1addlem4OLD  24873  itg10a  24884  itg1ge0a  24885  mbfi1fseqlem4  24892  itg2gt0  24934  limciun  25067  perfdvf  25076  cpnord  25108  dvcj  25123  dvlip2  25168  dvivth  25183  dvne0  25184  dvcnvre  25192  ply1lpir  25352  plyco0  25362  plyexmo  25482  abelth  25609  efif1o  25711  logno1  25800  efopnlem2  25821  loglesqrt  25920  lgamcvg2  26213  ppisval  26262  ppinprm  26310  chtnprm  26312  fsumvma  26370  dchrfi  26412  chtppilimlem2  26631  chebbnd2  26634  vmadivsumb  26640  rplogsumlem2  26642  dchrisumlem2  26647  vmalogdivsum2  26695  vmalogdivsum  26696  2vmadivsumlem  26697  selbergb  26706  selberg2b  26709  selberg3lem1  26714  selberg3lem2  26715  selberg3  26716  selberg4lem1  26717  selberg4  26718  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  uhgredgss  27510  usgruspgrb  27560  uhgrissubgr  27651  uhgrspansubgrlem  27666  uhgrspan1  27679  cusgredg  27800  usgredgsscusgredg  27835  ococss  29664  shsub1  29695  shless  29730  shmodsi  29760  pjhth  29764  spansnss  29942  spanpr  29951  spansnm0i  30021  pjjsi  30071  sumdmdii  30786  sumdmdlem  30789  sumdmdlem2  30790  cdj3lem1  30805  abrexss  30866  fnpreimac  31017  rnmposs  31020  unifi3  31056  uzssico  31114  ssnnssfz  31117  pwrssmgc  31287  pmtrcnel  31367  cycpmrn  31419  cyc3evpm  31426  cycpmgcl  31429  ringlsmss1  31593  ringlsmss2  31594  prmidlssidl  31629  dimkerim  31717  extdg1id  31747  crefss  31808  cmpcref  31809  zarmxt1  31839  tpr2rico  31871  esumrnmpt2  32045  esumpcvgval  32055  ldsysgenld  32137  sigapildsys  32139  ldgenpisys  32143  cldssbrsiga  32164  measdivcstALTV  32202  mbfmcnt  32244  oddpwdc  32330  eulerpartlemgs2  32356  reprpmtf1o  32615  bnj1033  32958  bnj1398  33023  sconnpi1  33210  cvmscld  33244  cvmliftlem15  33269  satfrnmapom  33341  dfon2lem6  33773  oldssmade  34069  sltlpss  34096  fnessref  34555  fgmin  34568  tailfb  34575  dissneqlem  35520  icoreresf  35532  rdglimss  35557  finxpreclem6  35576  lindsenlbs  35781  poimirlem11  35797  poimirlem12  35798  sstotbnd3  35943  prdstotbnd  35961  cntotbnd  35963  ismtyhmeo  35972  1idl  36193  lshpdisj  37008  lssats  37033  lkrin  37185  glbconxN  37399  paddss1  37838  paddss2  37839  paddasslem16  37856  paddidm  37862  pmodlem2  37868  pmapjoin  37873  pmapjat1  37874  pclfinN  37921  pclfinclN  37971  diasslssN  39080  dia2dimlem12  39096  dihsslss  39297  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  dvrelog2  40079  dvrelog3  40080  aks4d1p3  40093  aks4d1p4  40094  aks4d1p5  40095  aks4d1p7  40098  aks4d1p8  40102  sticksstones3  40111  eldiophss  40603  rencldnfilem  40649  pellexlem5  40662  pell14qrss1234  40685  pell1qrss14  40697  pellfundre  40710  pellfundge  40711  pellfundlb  40713  pellfundglb  40714  harinf  40863  proot1hash  41032  intabssd  41133  ss2iundf  41274  ov2ssiunov2  41315  clsk1indlem3  41660  finnzfsuppd  41827  radcnvrat  41939  nznngen  41941  trsspwALT3  42447  sspwimpALT2  42555  refsumcn  42580  iinssf  42694  icoiccdif  43069  icccncfext  43435  stoweidlem27  43575  stoweidlem46  43594  stoweidlem57  43605  fourierdlem40  43695  fourierdlem78  43732  ffnafv  44674  iccpartrn  44893  sprsymrelfvlem  44953  sprsymrelf1lem  44954  rnghmsscmap2  45542  rnghmsscmap  45543  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap2  45588  rhmsscmap  45589  rhmsscrnghm  45595  rngcresringcat  45599  funcringcsetc  45604  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  rhmsubcALTVlem4  45676  ssnn0ssfz  45696  lincolss  45786  lcoss  45788  lcosslsp  45790  iunord  46393