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

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  eqelssd  3958  ss2abim  4014  ss2abdv  4019  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  eq0rdvALT  4373  sspw  4573  elpwdifsn  4757  uniss  4880  intss1  4928  intmin  4933  intssuni  4935  iinssiun  4970  iunss1  4971  iinss1  4972  ss2iun  4975  ssiun  5011  ssiun2  5012  iinss  5021  iinss2  5022  iunxdif3  5061  sspwb  5430  pwssun  5553  relop  5836  dmss  5892  dmcosseq  5968  dmcosseqOLD  5969  ssrnres  6176  sossfld  6184  imadifssran  6202  imadifssranOLD  6203  predtrss  6323  preddowncl  6333  tron  6383  tz7.7  6386  funimassd  6947  dffv2  6976  chfnrn  7044  fvn0ssdmfun  7069  fveqdmss  7073  dff3  7095  ffnfv  7114  f1imass  7262  ssorduni  7774  onint  7785  limsssuc  7842  limuni3  7844  limomss  7863  fo1stres  8008  fo2ndres  8009  fo2ndf  8112  fnse  8125  ressuppssdif  8177  suppss  8186  reldmtpos  8226  fprlem2  8294  onfununi  8324  smoiun  8344  smocdmdom  8351  tz7.48-1  8426  tz7.49  8428  oaass  8542  cofon1  8654  cofon2  8655  qsss  8769  uniinqs  8791  pmss12g  8863  mapss  8883  ixpssmap2g  8921  ixpssmapg  8922  pssnn  9149  fineqv  9223  unifi3  9315  finnzfsuppd  9329  ssfii  9375  dffi2  9379  oismo  9498  unxpwdom2  9546  inf3lemd  9592  inf3lem1  9593  inf3lem6  9598  cantnflem3  9656  cantnf  9658  cnfcom3lem  9668  onssr1  9799  rankunb  9818  tcrank  9852  harcard  9960  carduni  9963  infxpenlem  9993  infpwfien  10042  dfac12r  10126  ackbij2lem1  10197  ackbij1lem18  10215  isfin1-3  10365  fin1a2lem11  10389  fin1a2lem13  10391  zorn2lem4  10478  zorn2lem5  10479  ttukeylem6  10493  ttukeylem7  10494  fpwwe2lem10  10620  fpwwe2lem11  10621  fpwwe2  10623  wunr1om  10699  wunom  10700  tskr1om  10747  tskr1om2  10748  tskxpss  10752  tskcard  10761  tskuni  10763  grothomex  10809  genpss  10984  distrlem1pr  11005  distrlem5pr  11007  ltexprlem2  11017  ltexprlem6  11021  ltexprlem7  11022  reclem3pr  11029  reclem4pr  11030  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  peano5uzi  12680  uzss  12880  ixxdisj  13382  ixxss1  13385  ixxss2  13386  ixxss12  13387  ixxub  13388  ixxlb  13389  iocssre  13449  icossre  13450  iccssre  13451  icodisj  13498  fzss1  13587  fzss2  13588  ssfzunsnext  13593  fzosplit  13717  fzouzsplit  13719  ssfzo12bi  13786  ssnn0fi  14017  fsuppmapnn0fiub  14023  suppssfz  14026  sswrd  14555  rtrclreclem3  15093  isercoll  15715  summolem2a  15762  fsumcvg3  15776  fsum2dlem  15817  fsumcom2  15821  qshash  15875  prodmolem2a  15984  fprod2dlem  16030  fprodcom2  16034  bitsfzo  16488  1arith  16982  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  ramtlecl  17055  prmgaplem3  17108  prmgaplem4  17109  monhom  17787  epihom  17794  funcsetcres2  18145  funcestrcsetclem8  18198  funcsetcestrclem8  18213  psdmrn  18624  chnrss  18666  chndss  18667  gsumwspan  18900  frmdss2  18917  sursubmefmnd  18950  injsubmefmnd  18951  trivsubgsnd  19215  ssnmz  19227  trivnsgd  19233  kerf1ghm  19312  conjnmz  19317  symgvalstruct  19462  gex1  19656  sylow2alem1  19682  lsmless1x  19709  lsmless2x  19710  lsmub1x  19711  lsmub2x  19712  lsmmod  19740  lsmdisj2  19747  efgrelexlemb  19815  efgcpbllemb  19820  cntzcmn  19905  gsum2d2  20039  dprdub  20092  dprdss  20096  dprddisj2  20106  pgpfac1lem3  20144  subrngmre  20661  subrguss  20686  subrgmre  20696  rnghmsscmap2  20728  rnghmsscmap  20729  funcrngcsetc  20739  funcrngcsetcALT  20740  rhmsscmap2  20757  rhmsscmap  20758  rhmsscrnghm  20764  rngcresringcat  20768  funcringcsetc  20773  unitrrg  20802  isdrng2  20843  primefld0cl  20909  primefld1cl  20910  lssssr  21075  lsssssubg  21079  lssmre  21087  lbspss  21203  lspdisj  21249  lbsextlem2  21283  lidl1el  21351  drngnidl  21377  prmidlssidl  21470  lpiss  21497  zsssubrg  21575  qsssubdrg  21576  cnsubrg  21577  mulgrhm2  21628  znrrg  21715  ocvocv  21821  ocv2ss  21823  ocvin  21824  lsmcss  21842  cssmre  21843  pjcss  21866  lindfrn  21971  sraassab  22018  mhpsubg  22316  evls1maprnss  22538  dmatsgrp  22656  scmatsgrp  22676  scmatsgrp1  22679  m2cpmrngiso  22915  bastg  23123  tgss  23125  tgtop  23130  tgidm  23137  en2top  23142  neisspw  23264  topssnei  23281  neiptopuni  23287  lpss3  23301  clslp  23305  tgrest  23316  ssrest  23333  restntr  23339  ordtbas2  23348  ordtbas  23349  cnss1  23433  cnss2  23434  cnsscnp  23436  cnrest2r  23444  cmpsublem  23556  cmpsub  23557  tgcmp  23558  cmpcld  23559  hauscmplem  23563  cnconn  23579  llyss  23636  nllyss  23637  restnlly  23639  restlly  23640  locfincmp  23683  locfincf  23688  kgenss  23700  kgenidm  23704  llycmpkgen2  23707  1stckgen  23711  kgen2ss  23712  kgencn3  23715  ptbasfi  23738  ptpjopn  23769  txdis  23789  txkgen  23809  xkoptsub  23811  xkopjcn  23813  txconn  23846  qtoptop2  23856  qtopuni  23859  qtopkgen  23867  basqtop  23868  tgqtop  23869  qtopss  23872  qtoprest  23874  qtopomap  23875  qtopcmap  23876  kqsat  23888  kqcldsat  23890  hmphdis  23953  isfild  24015  ssfg  24029  fgss  24030  fgss2  24031  fgfil  24032  fgabs  24036  filconn  24040  fgtr  24047  uzrest  24054  ufilmax  24064  ufileu  24076  filufint  24077  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem4  24114  flimss2  24129  flimss1  24130  flimclsi  24135  flimcf  24139  flimsncls  24143  fclssscls  24175  fclsss1  24179  fclsss2  24180  fclscf  24182  uffclsflim  24188  alexsublem  24201  alexsubALTlem3  24206  ptcmplem2  24210  ptcmplem3  24211  cnextf  24223  efmndtmd  24258  symgtgp  24263  cldsubg  24268  tsmscl  24292  haustsms2  24294  tgptsmscls  24307  tsmsxp  24312  restutop  24394  ustuqtop4  24401  utop2nei  24407  utop3cls  24408  ucncn  24441  xblss2ps  24558  xblss2  24559  xrsblre  24969  xrsmopn  24970  recld2  24972  zdis  24974  icccmplem2  24981  cncfss  25058  cnheiborlem  25113  htpycn  25132  phtpyhtpy  25141  pi1blem  25198  cphsscph  25410  cfilfcls  25433  iscmet3lem2  25451  iscmet2  25453  caussi  25456  equivcfil  25458  lmcau  25472  metsscmetcld  25474  hlhil  25602  ivthicc  25617  ovoliunnul  25666  ovolicopnf  25683  uniioombllem3  25744  dyadmbllem  25758  volsup2  25764  vitalilem2  25768  itg1addlem4  25858  itg10a  25869  itg1ge0a  25870  mbfi1fseqlem4  25877  itg2gt0  25919  limciun  26053  perfdvf  26062  cpnord  26094  dvcj  26109  dvlip2  26154  dvivth  26169  dvne0  26170  dvcnvre  26178  ply1lpir  26339  plyco0  26349  plyexmo  26474  abelth  26604  efif1o  26711  logno1  26801  efopnlem2  26822  loglesqrt  26926  lgamcvg2  27219  ppisval  27268  ppinprm  27316  chtnprm  27318  fsumvma  27377  dchrfi  27419  chtppilimlem2  27638  chebbnd2  27641  vmadivsumb  27647  rplogsumlem2  27649  dchrisumlem2  27654  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  selbergb  27713  selberg2b  27716  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrlog2bndlem2  27742  pntrlog2bndlem4  27744  oldssmade  28060  ltslpss  28101  noseqrdgfn  28499  n0ssoldg  28546  peano5uzs  28597  elplnglnid  29065  lnincplng  29066  plngrotlem2  29070  prlngpln3  29199  uhgredgss  29481  usgruspgrb  29533  uhgrissubgr  29625  uhgrspansubgrlem  29640  uhgrspan1  29653  cusgredg  29774  usgredgsscusgredg  29809  ococss  31645  shsub1  31676  shless  31711  shmodsi  31741  pjhth  31745  spansnss  31923  spanpr  31932  spansnm0i  32002  pjjsi  32052  sumdmdii  32767  sumdmdlem  32770  sumdmdlem2  32771  cdj3lem1  32786  abrexss  32858  fnpreimac  33015  rnmposs  33018  uzssico  33129  ssnnssfz  33132  pwrssmgc  33320  pmtrcnel  33409  cycpmrn  33463  cyc3evpm  33470  cycpmgcl  33473  elrgspnlem1  33562  elrgspnlem3  33564  elrgspnlem4  33565  elrgspnsubrunlem2  33568  fldgensdrg  33635  ringlsmss1  33707  ringlsmss2  33708  mxidlirredi  33754  drngmxidl  33759  drngmxidlr  33760  1arithidomlem1  33825  1arithidom  33827  1arithufdlem2  33835  1arithufdlem3  33836  1arithufdlem4  33837  dfufd2lem  33839  ply1mulrtss  33872  esplyfvaln  33964  dimkerim  34017  extdg1id  34056  irngss  34077  irngssv  34078  algextdeglem8  34114  constrsscn  34130  constrsslem  34131  constrsdrg  34165  crefss  34239  cmpcref  34240  zarmxt1  34270  tpr2rico  34302  esumrnmpt2  34458  esumpcvgval  34468  ldsysgenld  34550  sigapildsys  34552  ldgenpisys  34556  cldssbrsiga  34577  measdivcstALTV  34615  mbfmcnt  34658  oddpwdc  34744  eulerpartlemgs2  34770  reprpmtf1o  35013  bnj1033  35357  bnj1398  35422  trssfir1om  35507  r1omhfb  35508  trssfir1omregs  35549  r1omhfbregs  35550  sconnpi1  35731  cvmscld  35765  cvmliftlem15  35790  satfrnmapom  35862  dfon2lem6  36278  fnessref  36868  fgmin  36881  tailfb  36888  dissneqlem  37986  icoreresf  37998  rdglimss  38023  finxpreclem6  38042  lindsenlbs  38266  poimirlem11  38282  poimirlem12  38283  sstotbnd3  38427  prdstotbnd  38445  cntotbnd  38447  ismtyhmeo  38456  1idl  38677  disjdmqsss  39554  lshpdisj  39761  lssats  39786  lkrin  39938  glbconxN  40152  paddss1  40591  paddss2  40592  paddasslem16  40609  paddidm  40615  pmodlem2  40621  pmapjoin  40626  pmapjat1  40627  pclfinN  40674  pclfinclN  40724  diasslssN  41833  dia2dimlem12  41849  dihsslss  42050  baerlem3lem2  42484  baerlem5alem2  42485  baerlem5blem2  42486  zndvdchrrhm  42740  dvrelog2  42831  dvrelog3  42832  aks4d1p3  42845  aks4d1p4  42846  aks4d1p5  42847  aks4d1p7  42850  aks4d1p8  42854  primrootsunit1  42864  primrootscoprmpow  42866  primrootscoprbij  42869  hashscontpow1  42888  aks6d1c4  42891  sticksstones3  42915  aks6d1c6lem3  42939  aks6d1c6isolem2  42942  aks6d1c6lem5  42944  rhmqusspan  42952  unitscyglem1  42962  unitscyglem4  42965  eldiophss  43505  rencldnfilem  43547  pellexlem5  43560  pell14qrss1234  43583  pell1qrss14  43595  pellfundre  43608  pellfundge  43609  pellfundlb  43611  pellfundglb  43612  harinf  43761  proot1hash  43922  safesnsupfiss  44141  intabssd  44245  ss2iundf  44385  ov2ssiunov2  44426  clsk1indlem3  44769  radcnvrat  45024  nznngen  45026  trsspwALT3  45528  sspwimpALT2  45636  refsumcn  45750  iinssf  45856  icoiccdif  46240  icccncfext  46601  stoweidlem27  46741  stoweidlem46  46760  stoweidlem57  46771  fourierdlem40  46861  fourierdlem78  46898  ffnafv  47908  iccpartrn  48179  sprsymrelfvlem  48239  sprsymrelf1lem  48240  clnbgrssedg  48606  stgrusgra  48724  rhmsubcALTVlem4  49049  funcringcsetcALTV2lem8  49062  funcringcsetclem8ALTV  49085  ssnn0ssfz  49129  lincolss  49214  lcoss  49216  lcosslsp  49218  iunord  50454