Theorem ssrdv 3943

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ss 3922

This theorem is referenced by:  eqelssd  3959  ss2abdv  4020  sscon  4096  ssdif  4097  unss1  4138  ssrin  4195  eq0rdvALT  4361  sspw  4564  elpwdifsn  4743  uniss  4869  intss1  4916  intmin  4921  intssuni  4923  iinssiun  4958  iunss1  4959  iinss1  4960  ss2iun  4963  ssiun  4998  ssiun2  4999  iinss  5008  iinss2  5009  iunxdif3  5047  sspwb  5396  pwssun  5515  relop  5797  dmss  5849  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  imadifssran  6104  ssrnres  6131  sossfld  6139  predtrss  6274  preddowncl  6284  tron  6334  tz7.7  6337  funimassd  6893  dffv2  6922  chfnrn  6987  fvn0ssdmfun  7012  fveqdmss  7016  dff3  7038  ffnfv  7057  f1imass  7205  ssorduni  7719  onint  7730  limsssuc  7790  limuni3  7792  limomss  7811  fo1stres  7957  fo2ndres  7958  fo2ndf  8061  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  8597  cofon2  8598  qsss  8710  uniinqs  8731  pmss12g  8803  mapss  8823  ixpssmap2g  8861  ixpssmapg  8862  pssnn  9092  fineqv  9168  finnzfsuppd  9282  ssfii  9328  dffi2  9332  oismo  9451  unxpwdom2  9499  inf3lemd  9542  inf3lem1  9543  inf3lem6  9548  cantnflem3  9606  cantnf  9608  cnfcom3lem  9618  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  10553  fpwwe2lem11  10554  fpwwe2  10556  wunr1om  10632  wunom  10633  tskr1om  10680  tskr1om2  10681  tskxpss  10685  tskcard  10694  tskuni  10696  grothomex  10742  genpss  10917  distrlem1pr  10938  distrlem5pr  10940  ltexprlem2  10950  ltexprlem6  10954  ltexprlem7  10955  reclem3pr  10962  reclem4pr  10963  supaddc  12110  supadd  12111  supmul1  12112  supmullem2  12114  peano5uzi  12583  uzss  12776  ixxdisj  13281  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  iocssre  13348  icossre  13349  iccssre  13350  icodisj  13397  fzss1  13484  fzss2  13485  ssfzunsnext  13490  fzosplit  13613  fzouzsplit  13615  ssfzo12bi  13682  ssnn0fi  13910  fsuppmapnn0fiub  13916  suppssfz  13919  sswrd  14447  rtrclreclem3  14985  isercoll  15593  summolem2a  15640  fsumcvg3  15654  fsum2dlem  15695  fsumcom2  15699  qshash  15752  prodmolem2a  15859  fprod2dlem  15905  fprodcom2  15909  bitsfzo  16364  1arith  16857  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  ramtlecl  16930  prmgaplem3  16983  prmgaplem4  16984  monhom  17660  epihom  17667  funcsetcres2  18018  funcestrcsetclem8  18071  funcsetcestrclem8  18086  psdmrn  18497  gsumwspan  18738  frmdss2  18755  sursubmefmnd  18788  injsubmefmnd  18789  trivsubgsnd  19051  ssnmz  19063  trivnsgd  19069  kerf1ghm  19144  conjnmz  19149  symgvalstruct  19294  gex1  19488  sylow2alem1  19514  lsmless1x  19541  lsmless2x  19542  lsmub1x  19543  lsmub2x  19544  lsmmod  19572  lsmdisj2  19579  efgrelexlemb  19647  efgcpbllemb  19652  cntzcmn  19737  gsum2d2  19871  dprdub  19924  dprdss  19928  dprddisj2  19938  pgpfac1lem3  19976  subrngmre  20465  subrguss  20490  subrgmre  20500  rnghmsscmap2  20532  rnghmsscmap  20533  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscmap2  20561  rhmsscmap  20562  rhmsscrnghm  20568  rngcresringcat  20572  funcringcsetc  20577  unitrrg  20606  isdrng2  20646  primefld0cl  20709  primefld1cl  20710  lssssr  20875  lsssssubg  20879  lssmre  20887  lbspss  21004  lspdisj  21050  lbsextlem2  21084  lidl1el  21151  drngnidl  21168  lpiss  21254  zsssubrg  21350  qsssubdrg  21351  cnsubrg  21352  mulgrhm2  21403  znrrg  21490  ocvocv  21596  ocv2ss  21598  ocvin  21599  lsmcss  21617  cssmre  21618  pjcss  21641  lindfrn  21746  sraassab  21793  mhpsubg  22056  evls1maprnss  22281  dmatsgrp  22402  scmatsgrp  22422  scmatsgrp1  22425  m2cpmrngiso  22661  bastg  22869  tgss  22871  tgtop  22876  tgidm  22883  en2top  22888  neisspw  23010  topssnei  23027  neiptopuni  23033  lpss3  23047  clslp  23051  tgrest  23062  ssrest  23079  restntr  23085  ordtbas2  23094  ordtbas  23095  cnss1  23179  cnss2  23180  cnsscnp  23182  cnrest2r  23190  cmpsublem  23302  cmpsub  23303  tgcmp  23304  cmpcld  23305  hauscmplem  23309  cnconn  23325  llyss  23382  nllyss  23383  restnlly  23385  restlly  23386  locfincmp  23429  locfincf  23434  kgenss  23446  kgenidm  23450  llycmpkgen2  23453  1stckgen  23457  kgen2ss  23458  kgencn3  23461  ptbasfi  23484  ptpjopn  23515  txdis  23535  txkgen  23555  xkoptsub  23557  xkopjcn  23559  txconn  23592  qtoptop2  23602  qtopuni  23605  qtopkgen  23613  basqtop  23614  tgqtop  23615  qtopss  23618  qtoprest  23620  qtopomap  23621  qtopcmap  23622  kqsat  23634  kqcldsat  23636  hmphdis  23699  isfild  23761  ssfg  23775  fgss  23776  fgss2  23777  fgfil  23778  fgabs  23782  filconn  23786  fgtr  23793  uzrest  23800  ufilmax  23810  ufileu  23822  filufint  23823  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  flimss2  23875  flimss1  23876  flimclsi  23881  flimcf  23885  flimsncls  23889  fclssscls  23921  fclsss1  23925  fclsss2  23926  fclscf  23928  uffclsflim  23934  alexsublem  23947  alexsubALTlem3  23952  ptcmplem2  23956  ptcmplem3  23957  cnextf  23969  efmndtmd  24004  symgtgp  24009  cldsubg  24014  tsmscl  24038  haustsms2  24040  tgptsmscls  24053  tsmsxp  24058  restutop  24141  ustuqtop4  24148  utop2nei  24154  utop3cls  24155  ucncn  24188  xblss2ps  24305  xblss2  24306  xrsblre  24716  xrsmopn  24717  recld2  24719  zdis  24721  icccmplem2  24728  cncfss  24808  cnheiborlem  24869  htpycn  24888  phtpyhtpy  24897  pi1blem  24955  cphsscph  25167  cfilfcls  25190  iscmet3lem2  25208  iscmet2  25210  caussi  25213  equivcfil  25215  lmcau  25229  metsscmetcld  25231  hlhil  25359  ivthicc  25375  ovoliunnul  25424  ovolicopnf  25441  uniioombllem3  25502  dyadmbllem  25516  volsup2  25522  vitalilem2  25526  itg1addlem4  25616  itg10a  25627  itg1ge0a  25628  mbfi1fseqlem4  25635  itg2gt0  25677  limciun  25811  perfdvf  25820  cpnord  25853  dvcj  25870  dvlip2  25916  dvivth  25931  dvne0  25932  dvcnvre  25940  ply1lpir  26103  plyco0  26113  plyexmo  26237  abelth  26367  efif1o  26471  logno1  26561  efopnlem2  26582  loglesqrt  26687  lgamcvg2  26981  ppisval  27030  ppinprm  27078  chtnprm  27080  fsumvma  27140  dchrfi  27182  chtppilimlem2  27401  chebbnd2  27404  vmadivsumb  27410  rplogsumlem2  27412  dchrisumlem2  27417  vmalogdivsum2  27465  vmalogdivsum  27466  2vmadivsumlem  27467  selbergb  27476  selberg2b  27479  selberg3lem1  27484  selberg3lem2  27485  selberg3  27486  selberg4lem1  27487  selberg4  27488  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  oldssmade  27809  sltlpss  27840  noseqrdgfn  28223  peano5uzs  28315  uhgredgss  29094  usgruspgrb  29146  uhgrissubgr  29238  uhgrspansubgrlem  29253  uhgrspan1  29266  cusgredg  29387  usgredgsscusgredg  29423  ococss  31255  shsub1  31286  shless  31321  shmodsi  31351  pjhth  31355  spansnss  31533  spanpr  31542  spansnm0i  31612  pjjsi  31662  sumdmdii  32377  sumdmdlem  32380  sumdmdlem2  32381  cdj3lem1  32396  abrexss  32474  fnpreimac  32628  rnmposs  32631  unifi3  32669  uzssico  32740  ssnnssfz  32743  pwrssmgc  32955  pmtrcnel  33044  cycpmrn  33098  cyc3evpm  33105  cycpmgcl  33108  elrgspnlem1  33195  elrgspnlem3  33197  elrgspnlem4  33198  elrgspnsubrunlem2  33201  fldgensdrg  33266  ringlsmss1  33346  ringlsmss2  33347  prmidlssidl  33395  mxidlirredi  33421  drngmxidl  33427  drngmxidlr  33428  1arithidomlem1  33485  1arithidom  33487  1arithufdlem2  33495  1arithufdlem3  33496  1arithufdlem4  33497  dfufd2lem  33499  ply1mulrtss  33529  dimkerim  33602  extdg1id  33640  irngss  33661  irngssv  33662  algextdeglem8  33693  constrsscn  33709  constrsslem  33710  constrsdrg  33744  crefss  33818  cmpcref  33819  zarmxt1  33849  tpr2rico  33881  esumrnmpt2  34037  esumpcvgval  34047  ldsysgenld  34129  sigapildsys  34131  ldgenpisys  34135  cldssbrsiga  34156  measdivcstALTV  34194  mbfmcnt  34238  oddpwdc  34324  eulerpartlemgs2  34350  reprpmtf1o  34596  bnj1033  34938  bnj1398  35003  sconnpi1  35214  cvmscld  35248  cvmliftlem15  35273  satfrnmapom  35345  dfon2lem6  35764  fnessref  36333  fgmin  36346  tailfb  36353  dissneqlem  37316  icoreresf  37328  rdglimss  37353  finxpreclem6  37372  lindsenlbs  37597  poimirlem11  37613  poimirlem12  37614  sstotbnd3  37758  prdstotbnd  37776  cntotbnd  37778  ismtyhmeo  37787  1idl  38008  disjdmqsss  38782  lshpdisj  38968  lssats  38993  lkrin  39145  glbconxN  39360  paddss1  39799  paddss2  39800  paddasslem16  39817  paddidm  39823  pmodlem2  39829  pmapjoin  39834  pmapjat1  39835  pclfinN  39882  pclfinclN  39932  diasslssN  41041  dia2dimlem12  41057  dihsslss  41258  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  zndvdchrrhm  41948  dvrelog2  42040  dvrelog3  42041  aks4d1p3  42054  aks4d1p4  42055  aks4d1p5  42056  aks4d1p7  42059  aks4d1p8  42063  primrootsunit1  42073  primrootscoprmpow  42075  primrootscoprbij  42078  hashscontpow1  42097  aks6d1c4  42100  sticksstones3  42124  aks6d1c6lem3  42148  aks6d1c6isolem2  42151  aks6d1c6lem5  42153  rhmqusspan  42161  unitscyglem1  42171  unitscyglem4  42174  ss2ab1  42195  eldiophss  42750  rencldnfilem  42796  pellexlem5  42809  pell14qrss1234  42832  pell1qrss14  42844  pellfundre  42857  pellfundge  42858  pellfundlb  42860  pellfundglb  42861  harinf  43010  proot1hash  43171  safesnsupfiss  43391  intabssd  43495  ss2iundf  43635  ov2ssiunov2  43676  clsk1indlem3  44019  radcnvrat  44290  nznngen  44292  trsspwALT3  44796  sspwimpALT2  44904  refsumcn  45011  iinssf  45119  icoiccdif  45509  icccncfext  45872  stoweidlem27  46012  stoweidlem46  46031  stoweidlem57  46042  fourierdlem40  46132  fourierdlem78  46169  ffnafv  47159  iccpartrn  47418  sprsymrelfvlem  47478  sprsymrelf1lem  47479  clnbgrssedg  47829  stgrusgra  47947  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  ssnn0ssfz  48337  lincolss  48423  lcoss  48425  lcosslsp  48427  iunord  49665