Theorem ssrdv 3989

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108   ⊆ wss 3951

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 3968

This theorem is referenced by:  eqelssd  4005  ss2abdv  4066  sscon  4143  ssdif  4144  unss1  4185  ssrin  4242  eq0rdvALT  4408  sspw  4611  elpwdifsn  4789  uniss  4915  intss1  4963  intmin  4968  intssuni  4970  iinssiun  5005  iunss1  5006  iinss1  5007  ss2iun  5010  ssiun  5046  ssiun2  5047  iinss  5056  iinss2  5057  iunxdif3  5095  sspwb  5454  pwssun  5575  relop  5861  dmss  5913  dmcosseq  5987  dmcosseqOLD  5988  imadifssran  6171  ssrnres  6198  sossfld  6206  predtrss  6343  preddowncl  6353  tron  6407  tz7.7  6410  funimassd  6975  dffv2  7004  chfnrn  7069  fvn0ssdmfun  7094  fveqdmss  7098  dff3  7120  ffnfv  7139  f1imass  7284  ssorduni  7799  onint  7810  limsssuc  7871  limuni3  7873  limomss  7892  fo1stres  8040  fo2ndres  8041  fo2ndf  8146  fnse  8158  ressuppssdif  8210  suppss  8219  reldmtpos  8259  fprlem2  8326  onfununi  8381  smoiun  8401  smocdmdom  8408  tz7.48-1  8483  tz7.49  8485  oaass  8599  cofon1  8710  cofon2  8711  qsss  8818  uniinqs  8837  pmss12g  8909  mapss  8929  ixpssmap2g  8967  ixpssmapg  8968  pssnn  9208  fineqv  9299  finnzfsuppd  9413  ssfii  9459  dffi2  9463  oismo  9580  unxpwdom2  9628  inf3lemd  9667  inf3lem1  9668  inf3lem6  9673  cantnflem3  9731  cantnf  9733  cnfcom3lem  9743  onssr1  9871  rankunb  9890  tcrank  9924  harcard  10018  carduni  10021  infxpenlem  10053  infpwfien  10102  dfac12r  10187  ackbij2lem1  10258  ackbij1lem18  10276  isfin1-3  10426  fin1a2lem11  10450  fin1a2lem13  10452  zorn2lem4  10539  zorn2lem5  10540  ttukeylem6  10554  ttukeylem7  10555  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2  10683  wunr1om  10759  wunom  10760  tskr1om  10807  tskr1om2  10808  tskxpss  10812  tskcard  10821  tskuni  10823  grothomex  10869  genpss  11044  distrlem1pr  11065  distrlem5pr  11067  ltexprlem2  11077  ltexprlem6  11081  ltexprlem7  11082  reclem3pr  11089  reclem4pr  11090  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  peano5uzi  12707  uzss  12901  ixxdisj  13402  ixxss1  13405  ixxss2  13406  ixxss12  13407  ixxub  13408  ixxlb  13409  iocssre  13467  icossre  13468  iccssre  13469  icodisj  13516  fzss1  13603  fzss2  13604  ssfzunsnext  13609  fzosplit  13732  fzouzsplit  13734  ssfzo12bi  13800  ssnn0fi  14026  fsuppmapnn0fiub  14032  suppssfz  14035  sswrd  14560  rtrclreclem3  15099  isercoll  15704  summolem2a  15751  fsumcvg3  15765  fsum2dlem  15806  fsumcom2  15810  qshash  15863  prodmolem2a  15970  fprod2dlem  16016  fprodcom2  16020  bitsfzo  16472  1arith  16965  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  ramtlecl  17038  prmgaplem3  17091  prmgaplem4  17092  monhom  17779  epihom  17786  funcsetcres2  18138  funcestrcsetclem8  18192  funcsetcestrclem8  18207  psdmrn  18618  gsumwspan  18859  frmdss2  18876  sursubmefmnd  18909  injsubmefmnd  18910  trivsubgsnd  19172  ssnmz  19184  trivnsgd  19190  kerf1ghm  19265  conjnmz  19270  symgvalstruct  19414  symgvalstructOLD  19415  gex1  19609  sylow2alem1  19635  lsmless1x  19662  lsmless2x  19663  lsmub1x  19664  lsmub2x  19665  lsmmod  19693  lsmdisj2  19700  efgrelexlemb  19768  efgcpbllemb  19773  cntzcmn  19858  gsum2d2  19992  dprdub  20045  dprdss  20049  dprddisj2  20059  pgpfac1lem3  20097  subrngmre  20562  subrguss  20587  subrgmre  20597  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  rngcresringcat  20669  funcringcsetc  20674  unitrrg  20703  isdrng2  20743  primefld0cl  20807  primefld1cl  20808  lssssr  20952  lsssssubg  20956  lssmre  20964  lbspss  21081  lspdisj  21127  lbsextlem2  21161  lidl1el  21236  drngnidl  21253  lpiss  21339  zsssubrg  21443  qsssubdrg  21444  cnsubrg  21445  mulgrhm2  21489  znrrg  21584  ocvocv  21689  ocv2ss  21691  ocvin  21692  lsmcss  21710  cssmre  21711  pjcss  21736  lindfrn  21841  sraassab  21888  mhpsubg  22157  evls1maprnss  22382  dmatsgrp  22505  scmatsgrp  22525  scmatsgrp1  22528  m2cpmrngiso  22764  bastg  22973  tgss  22975  tgtop  22980  tgidm  22987  en2top  22992  neisspw  23115  topssnei  23132  neiptopuni  23138  lpss3  23152  clslp  23156  tgrest  23167  ssrest  23184  restntr  23190  ordtbas2  23199  ordtbas  23200  cnss1  23284  cnss2  23285  cnsscnp  23287  cnrest2r  23295  cmpsublem  23407  cmpsub  23408  tgcmp  23409  cmpcld  23410  hauscmplem  23414  cnconn  23430  llyss  23487  nllyss  23488  restnlly  23490  restlly  23491  locfincmp  23534  locfincf  23539  kgenss  23551  kgenidm  23555  llycmpkgen2  23558  1stckgen  23562  kgen2ss  23563  kgencn3  23566  ptbasfi  23589  ptpjopn  23620  txdis  23640  txkgen  23660  xkoptsub  23662  xkopjcn  23664  txconn  23697  qtoptop2  23707  qtopuni  23710  qtopkgen  23718  basqtop  23719  tgqtop  23720  qtopss  23723  qtoprest  23725  qtopomap  23726  qtopcmap  23727  kqsat  23739  kqcldsat  23741  hmphdis  23804  isfild  23866  ssfg  23880  fgss  23881  fgss2  23882  fgfil  23883  fgabs  23887  filconn  23891  fgtr  23898  uzrest  23905  ufilmax  23915  ufileu  23927  filufint  23928  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  flimss2  23980  flimss1  23981  flimclsi  23986  flimcf  23990  flimsncls  23994  fclssscls  24026  fclsss1  24030  fclsss2  24031  fclscf  24033  uffclsflim  24039  alexsublem  24052  alexsubALTlem3  24057  ptcmplem2  24061  ptcmplem3  24062  cnextf  24074  efmndtmd  24109  symgtgp  24114  cldsubg  24119  tsmscl  24143  haustsms2  24145  tgptsmscls  24158  tsmsxp  24163  restutop  24246  ustuqtop4  24253  utop2nei  24259  utop3cls  24260  ucncn  24294  xblss2ps  24411  xblss2  24412  xrsblre  24833  xrsmopn  24834  recld2  24836  zdis  24838  icccmplem2  24845  cncfss  24925  cnheiborlem  24986  htpycn  25005  phtpyhtpy  25014  pi1blem  25072  cphsscph  25285  cfilfcls  25308  iscmet3lem2  25326  iscmet2  25328  caussi  25331  equivcfil  25333  lmcau  25347  metsscmetcld  25349  hlhil  25477  ivthicc  25493  ovoliunnul  25542  ovolicopnf  25559  uniioombllem3  25620  dyadmbllem  25634  volsup2  25640  vitalilem2  25644  itg1addlem4  25734  itg10a  25745  itg1ge0a  25746  mbfi1fseqlem4  25753  itg2gt0  25795  limciun  25929  perfdvf  25938  cpnord  25971  dvcj  25988  dvlip2  26034  dvivth  26049  dvne0  26050  dvcnvre  26058  ply1lpir  26221  plyco0  26231  plyexmo  26355  abelth  26485  efif1o  26588  logno1  26678  efopnlem2  26699  loglesqrt  26804  lgamcvg2  27098  ppisval  27147  ppinprm  27195  chtnprm  27197  fsumvma  27257  dchrfi  27299  chtppilimlem2  27518  chebbnd2  27521  vmadivsumb  27527  rplogsumlem2  27529  dchrisumlem2  27534  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  selbergb  27593  selberg2b  27596  selberg3lem1  27601  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  oldssmade  27916  sltlpss  27945  noseqrdgfn  28312  peano5uzs  28390  uhgredgss  29148  usgruspgrb  29200  uhgrissubgr  29292  uhgrspansubgrlem  29307  uhgrspan1  29320  cusgredg  29441  usgredgsscusgredg  29477  ococss  31312  shsub1  31343  shless  31378  shmodsi  31408  pjhth  31412  spansnss  31590  spanpr  31599  spansnm0i  31669  pjjsi  31719  sumdmdii  32434  sumdmdlem  32437  sumdmdlem2  32438  cdj3lem1  32453  abrexss  32531  fnpreimac  32681  rnmposs  32684  unifi3  32724  uzssico  32786  ssnnssfz  32789  pwrssmgc  32990  pmtrcnel  33109  cycpmrn  33163  cyc3evpm  33170  cycpmgcl  33173  elrgspnlem1  33246  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem2  33252  fldgensdrg  33316  ringlsmss1  33424  ringlsmss2  33425  prmidlssidl  33473  mxidlirredi  33499  drngmxidl  33505  drngmxidlr  33506  1arithidomlem1  33563  1arithidom  33565  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  ply1mulrtss  33606  dimkerim  33678  extdg1id  33716  irngss  33737  irngssv  33738  algextdeglem8  33765  constrsscn  33781  constrsslem  33782  crefss  33848  cmpcref  33849  zarmxt1  33879  tpr2rico  33911  esumrnmpt2  34069  esumpcvgval  34079  ldsysgenld  34161  sigapildsys  34163  ldgenpisys  34167  cldssbrsiga  34188  measdivcstALTV  34226  mbfmcnt  34270  oddpwdc  34356  eulerpartlemgs2  34382  reprpmtf1o  34641  bnj1033  34983  bnj1398  35048  sconnpi1  35244  cvmscld  35278  cvmliftlem15  35303  satfrnmapom  35375  dfon2lem6  35789  fnessref  36358  fgmin  36371  tailfb  36378  dissneqlem  37341  icoreresf  37353  rdglimss  37378  finxpreclem6  37397  lindsenlbs  37622  poimirlem11  37638  poimirlem12  37639  sstotbnd3  37783  prdstotbnd  37801  cntotbnd  37803  ismtyhmeo  37812  1idl  38033  disjdmqsss  38803  lshpdisj  38988  lssats  39013  lkrin  39165  glbconxN  39380  paddss1  39819  paddss2  39820  paddasslem16  39837  paddidm  39843  pmodlem2  39849  pmapjoin  39854  pmapjat1  39855  pclfinN  39902  pclfinclN  39952  diasslssN  41061  dia2dimlem12  41077  dihsslss  41278  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  zndvdchrrhm  41972  dvrelog2  42065  dvrelog3  42066  aks4d1p3  42079  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8  42088  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  hashscontpow1  42122  aks6d1c4  42125  sticksstones3  42149  aks6d1c6lem3  42173  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  rhmqusspan  42186  unitscyglem1  42196  unitscyglem4  42199  ss2ab1  42258  eldiophss  42785  rencldnfilem  42831  pellexlem5  42844  pell14qrss1234  42867  pell1qrss14  42879  pellfundre  42892  pellfundge  42893  pellfundlb  42895  pellfundglb  42896  harinf  43046  proot1hash  43207  safesnsupfiss  43428  intabssd  43532  ss2iundf  43672  ov2ssiunov2  43713  clsk1indlem3  44056  radcnvrat  44333  nznngen  44335  trsspwALT3  44840  sspwimpALT2  44948  refsumcn  45035  iinssf  45143  icoiccdif  45537  icccncfext  45902  stoweidlem27  46042  stoweidlem46  46061  stoweidlem57  46072  fourierdlem40  46162  fourierdlem78  46199  ffnafv  47183  iccpartrn  47417  sprsymrelfvlem  47477  sprsymrelf1lem  47478  clnbgrssedg  47827  stgrusgra  47926  rhmsubcALTVlem4  48200  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  ssnn0ssfz  48265  lincolss  48351  lcoss  48353  lcosslsp  48355  iunord  49195