Theorem ssrdv 3937

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ss 3916

This theorem is used by:  eqelssd  3952  ss2abim  4008  ss2abdv  4013  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  eq0rdvALT  4366  sspw  4568  elpwdifsn  4752  uniss  4875  intss1  4923  intmin  4928  intssuni  4930  iinssiun  4965  iunss1  4966  iinss1  4967  ss2iun  4970  ssiun  5005  ssiun2  5006  iinss  5015  iinss2  5016  iunxdif3  5055  sspwb  5424  pwssun  5547  relop  5830  dmss  5886  dmcosseq  5962  dmcosseqOLD  5963  ssrnres  6171  sossfld  6179  imadifssran  6197  imadifssranOLD  6198  predtrss  6320  preddowncl  6330  tron  6380  tz7.7  6383  funimassd  6944  dffv2  6973  chfnrn  7041  fvn0ssdmfun  7067  fveqdmss  7071  dff3  7093  ffnfv  7112  f1imass  7261  ssorduni  7778  onint  7789  limsssuc  7846  limuni3  7848  limomss  7867  fo1stres  8012  fo2ndres  8013  fo2ndf  8118  fnse  8131  ressuppssdif  8183  suppss  8192  reldmtpos  8232  fprlem2  8300  onfununi  8330  smoiun  8350  smocdmdom  8357  tz7.48-1  8432  tz7.49  8434  oaass  8548  cofon1  8660  cofon2  8661  qsss  8775  uniinqs  8797  pmss12g  8876  mapss  8896  ixpssmap2g  8934  ixpssmapg  8935  pssnn  9163  fineqv  9237  unifi3  9329  finnzfsuppd  9343  ssfii  9389  dffi2  9393  oismo  9512  unxpwdom2  9560  inf3lemd  9606  inf3lem1  9607  inf3lem6  9612  cantnflem3  9670  cantnf  9672  cnfcom3lem  9682  onssr1  9813  rankunb  9832  tcrank  9866  harcard  9983  carduni  9986  infxpenlem  10016  infpwfien  10065  dfac12r  10149  ackbij2lem1  10220  ackbij1lem18  10238  isfin1-3  10388  fin1a2lem11  10412  fin1a2lem13  10414  zorn2lem4  10501  zorn2lem5  10502  ttukeylem6  10516  ttukeylem7  10517  fpwwe2lem10  10649  fpwwe2lem11  10650  fpwwe2  10652  wunr1om  10728  wunom  10729  tskr1om  10776  tskr1om2  10777  tskxpss  10781  tskcard  10790  tskuni  10792  grothomex  10838  genpss  11013  distrlem1pr  11034  distrlem5pr  11036  ltexprlem2  11046  ltexprlem6  11050  ltexprlem7  11051  reclem3pr  11058  reclem4pr  11059  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  peano5uzi  12710  uzss  12910  ixxdisj  13413  ixxss1  13416  ixxss2  13417  ixxss12  13418  ixxub  13419  ixxlb  13420  iocssre  13480  icossre  13481  iccssre  13482  icodisj  13529  fzss1  13618  fzss2  13619  ssfzunsnext  13624  fzosplit  13748  fzouzsplit  13750  ssfzo12bi  13817  ssnn0fi  14049  fsuppmapnn0fiub  14055  suppssfz  14058  sswrd  14587  rtrclreclem3  15133  isercoll  15755  summolem2a  15801  fsumcvg3  15815  fsum2dlem  15856  fsumcom2  15860  qshash  15914  prodmolem2a  16021  fprod2dlem  16067  fprodcom2  16071  bitsfzo  16525  1arith  17019  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  ramtlecl  17092  prmgaplem3  17145  prmgaplem4  17146  monhom  17824  epihom  17831  funcsetcres2  18182  funcestrcsetclem8  18235  funcsetcestrclem8  18250  psdmrn  18661  chnrss  18703  chndss  18704  gsumwspan  18955  frmdss2  18972  sursubmefmnd  19005  injsubmefmnd  19006  trivsubgsnd  19277  ssnmz  19289  trivnsgd  19295  kerf1ghm  19374  conjnmz  19379  symgvalstruct  19524  gex1  19718  sylow2alem1  19744  lsmless1x  19771  lsmless2x  19772  lsmub1x  19773  lsmub2x  19774  lsmmod  19802  lsmdisj2  19809  efgrelexlemb  19877  efgcpbllemb  19882  cntzcmn  19967  gsum2d2  20101  dprdub  20154  dprdss  20158  dprddisj2  20168  pgpfac1lem3  20206  subrngmre  20724  subrguss  20749  subrgmre  20759  rnghmsscmap2  20791  rnghmsscmap  20792  funcrngcsetc  20802  funcrngcsetcALT  20803  rhmsscmap2  20820  rhmsscmap  20821  rhmsscrnghm  20827  rngcresringcat  20831  funcringcsetc  20836  unitrrg  20865  isdrng2  20906  primefld0cl  20972  primefld1cl  20973  lssssr  21138  lsssssubg  21142  lssmre  21150  lbspss  21266  lspdisj  21312  lbsextlem2  21346  lidl1el  21414  drngnidl  21440  prmidlssidl  21533  lpiss  21560  zsssubrg  21638  qsssubdrg  21639  cnsubrg  21640  mulgrhm2  21691  znrrg  21778  ocvocv  21884  ocv2ss  21886  ocvin  21887  lsmcss  21905  cssmre  21906  pjcss  21929  lindfrn  22034  lindsenlbs  22064  sraassab  22083  mhpsubg  22381  evls1maprnss  22603  dmatsgrp  22721  scmatsgrp  22741  scmatsgrp1  22744  m2cpmrngiso  22983  bastg  23191  tgss  23193  tgtop  23198  tgidm  23205  en2top  23210  neisspw  23332  topssnei  23349  neiptopuni  23355  lpss3  23369  clslp  23373  tgrest  23384  ssrest  23401  restntr  23407  ordtbas2  23416  ordtbas  23417  cnss1  23501  cnss2  23502  cnsscnp  23504  cnrest2r  23512  cmpsublem  23624  cmpsub  23625  tgcmp  23626  cmpcld  23627  hauscmplem  23631  cnconn  23647  llyss  23705  nllyss  23706  restnlly  23708  restlly  23709  locfincmp  23752  locfincf  23757  kgenss  23769  kgenidm  23773  llycmpkgen2  23776  1stckgen  23780  kgen2ss  23781  kgencn3  23784  ptbasfi  23807  ptpjopn  23838  txdis  23858  txkgen  23878  xkoptsub  23880  xkopjcn  23882  txconn  23915  qtoptop2  23925  qtopuni  23928  qtopkgen  23936  basqtop  23937  tgqtop  23938  qtopss  23941  qtoprest  23943  qtopomap  23944  qtopcmap  23945  kqsat  23957  kqcldsat  23959  hmphdis  24022  isfild  24084  ssfg  24098  fgss  24099  fgss2  24100  fgfil  24101  fgabs  24105  filconn  24109  fgtr  24116  uzrest  24123  ufilmax  24133  ufileu  24145  filufint  24146  rnelfm  24179  fmfnfmlem2  24181  fmfnfmlem4  24183  flimss2  24198  flimss1  24199  flimclsi  24204  flimcf  24208  flimsncls  24212  fclssscls  24244  fclsss1  24248  fclsss2  24249  fclscf  24251  uffclsflim  24257  alexsublem  24270  alexsubALTlem3  24275  ptcmplem2  24279  ptcmplem3  24280  cnextf  24292  efmndtmd  24327  symgtgp  24332  cldsubg  24337  tsmscl  24361  haustsms2  24363  tgptsmscls  24376  tsmsxp  24381  restutop  24463  ustuqtop4  24470  utop2nei  24476  utop3cls  24477  ucncn  24510  xblss2ps  24627  xblss2  24628  xrsblre  25038  xrsmopn  25039  recld2  25041  zdis  25043  icccmplem2  25050  cncfss  25127  cnheiborlem  25182  htpycn  25201  phtpyhtpy  25210  pi1blem  25267  cphsscph  25479  cfilfcls  25502  iscmet3lem2  25520  iscmet2  25522  caussi  25525  equivcfil  25527  lmcau  25541  metsscmetcld  25543  hlhil  25671  ivthicc  25686  ovoliunnul  25735  ovolicopnf  25752  uniioombllem3  25813  dyadmbllem  25827  volsup2  25833  vitalilem2  25837  itg1addlem4  25927  itg10a  25938  itg1ge0a  25939  mbfi1fseqlem4  25946  itg2gt0  25988  limciun  26121  perfdvf  26130  cpnord  26162  dvcj  26177  dvlip2  26222  dvivth  26237  dvne0  26238  dvcnvre  26246  ply1lpir  26407  plyco0  26417  plyconz  26540  plyexmo  26545  abelth  26677  efif1o  26783  logno1  26873  efopnlem2  26894  loglesqrt  26998  lgamcvg2  27291  ppisval  27340  ppinprm  27388  chtnprm  27390  fsumvma  27449  dchrfi  27491  chtppilimlem2  27710  chebbnd2  27713  vmadivsumb  27719  rplogsumlem2  27721  dchrisumlem2  27726  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  selbergb  27785  selberg2b  27788  selberg3lem1  27793  selberg3lem2  27794  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrlog2bndlem2  27814  pntrlog2bndlem4  27816  oldssmade  28132  ltslpss  28173  noseqrdgfn  28571  n0ssoldg  28618  peano5uzs  28669  elplnglnid  29140  lnincplng  29141  plngrotlem2  29145  cgrabasimass  29257  prlngpln3  29306  uhgredgss  29588  usgruspgrb  29643  uhgrissubgr  29735  uhgrspansubgrlem  29750  uhgrspan1  29763  cusgredg  29884  usgredgsscusgredg  29919  ococss  31774  shsub1  31805  shless  31840  shmodsi  31870  pjhth  31874  spansnss  32052  spanpr  32061  spansnm0i  32131  pjjsi  32181  sumdmdii  32896  sumdmdlem  32899  sumdmdlem2  32900  cdj3lem1  32915  abrexss  32987  fnpreimac  33143  rnmposs  33146  uzssico  33255  ssnnssfz  33258  pwrssmgc  33440  pmtrcnel  33529  cycpmrn  33583  cyc3evpm  33590  cycpmgcl  33593  elrgspnlem1  33682  elrgspnlem3  33684  elrgspnlem4  33685  elrgspnsubrunlem2  33688  fldgensdrg  33755  ringlsmss1  33827  ringlsmss2  33828  mxidlirredi  33874  drngmxidl  33879  drngmxidlr  33880  1arithidomlem1  33945  1arithidom  33947  1arithufdlem2  33955  1arithufdlem3  33956  1arithufdlem4  33957  dfufd2lem  33959  ply1mulrtss  33992  esplyfvaln  34084  dimkerim  34137  extdg1id  34176  irngss  34197  irngssv  34198  algextdeglem8  34234  constrsscn  34250  constrsslem  34251  constrsdrg  34285  crefss  34359  cmpcref  34360  zarmxt1  34390  tpr2rico  34422  esumrnmpt2  34578  esumpcvgval  34588  ldsysgenld  34671  sigapildsys  34673  ldgenpisys  34677  cldssbrsiga  34698  measdivcstALTV  34736  mbfmcnt  34779  oddpwdc  34865  eulerpartlemgs2  34891  reprpmtf1o  35134  bnj1033  35478  bnj1398  35543  trssfir1om  35621  r1omhfb  35622  trssfir1omregs  35662  r1omhfbregs  35663  sconnpi1  35818  cvmscld  35852  cvmliftlem15  35877  satfrnmapom  35949  dfon2lem6  36365  fnessref  36976  fgmin  36989  tailfb  36996  dissneqlem  38094  icoreresf  38106  rdglimss  38131  finxpreclem6  38150  poimirlem11  38380  poimirlem12  38381  sstotbnd3  38526  prdstotbnd  38544  cntotbnd  38546  ismtyhmeo  38555  1idl  38776  disjdmqsss  39653  lshpdisj  39860  lssats  39885  lkrin  40037  glbconxN  40251  paddss1  40690  paddss2  40691  paddasslem16  40708  paddidm  40714  pmodlem2  40720  pmapjoin  40725  pmapjat1  40726  pclfinN  40773  pclfinclN  40823  diasslssN  41932  dia2dimlem12  41948  dihsslss  42149  baerlem3lem2  42583  baerlem5alem2  42584  baerlem5blem2  42585  zndvdchrrhm  42839  dvrelog2  42930  dvrelog3  42931  aks4d1p3  42944  aks4d1p4  42945  aks4d1p5  42946  aks4d1p7  42949  aks4d1p8  42953  primrootsunit1  42963  primrootscoprmpow  42965  primrootscoprbij  42968  hashscontpow1  42987  aks6d1c4  42990  sticksstones3  43014  aks6d1c6lem3  43038  aks6d1c6isolem2  43041  aks6d1c6lem5  43043  rhmqusspan  43051  unitscyglem1  43061  unitscyglem4  43064  eldiophss  43619  rencldnfilem  43661  pellexlem5  43674  pell14qrss1234  43697  pell1qrss14  43709  pellfundre  43722  pellfundge  43723  pellfundlb  43725  pellfundglb  43726  harinf  43875  proot1hash  44036  safesnsupfiss  44255  intabssd  44359  ss2iundf  44499  ov2ssiunov2  44540  clsk1indlem3  44883  radcnvrat  45138  nznngen  45140  trsspwALT3  45642  sspwimpALT2  45750  refsumcn  45864  iinssf  45970  icoiccdif  46354  icccncfext  46715  stoweidlem27  46855  stoweidlem46  46874  stoweidlem57  46885  fourierdlem40  46975  fourierdlem78  47012  ffnafv  48059  iccpartrn  48330  sprsymrelfvlem  48390  sprsymrelf1lem  48391  clnbgrssedg  48757  stgrusgra  48875  rhmsubcALTVlem4  49199  funcringcsetcALTV2lem8  49212  funcringcsetclem8ALTV  49235  ssnn0ssfz  49279  lincolss  49364  lcoss  49366  lcosslsp  49368  iunord  50602