Theorem ssrdv 4000

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

Syntax hints:   → wi 4  ∀wal 1534   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  eqelssd  4016  ss2abdv  4075  sscon  4152  ssdif  4153  unss1  4194  ssrin  4249  eq0rdvALT  4413  sspw  4615  elpwdifsn  4793  uniss  4919  intss1  4967  intmin  4972  intssuni  4974  iinssiun  5009  iunss1  5010  iinss1  5011  ss2iun  5014  ssiun  5050  ssiun2  5051  iinss  5060  iinss2  5061  iunxdif3  5099  sspwb  5459  pwssun  5579  relop  5863  dmss  5915  dmcosseq  5989  dmcosseqOLD  5990  ssrnres  6199  sossfld  6207  predtrss  6344  preddowncl  6354  tron  6408  tz7.7  6411  funimassd  6974  dffv2  7003  chfnrn  7068  fvn0ssdmfun  7093  fveqdmss  7097  dff3  7119  ffnfv  7138  f1imass  7283  ssorduni  7797  onint  7809  limsssuc  7870  limuni3  7872  limomss  7891  fo1stres  8038  fo2ndres  8039  fo2ndf  8144  fnse  8156  ressuppssdif  8208  suppss  8217  reldmtpos  8257  fprlem2  8324  onfununi  8379  smoiun  8399  smocdmdom  8406  tz7.48-1  8481  tz7.49  8483  oaass  8597  cofon1  8708  cofon2  8709  qsss  8816  uniinqs  8835  pmss12g  8907  mapss  8927  ixpssmap2g  8965  ixpssmapg  8966  pssnn  9206  fineqv  9296  finnzfsuppd  9410  ssfii  9456  dffi2  9460  oismo  9577  unxpwdom2  9625  inf3lemd  9664  inf3lem1  9665  inf3lem6  9670  cantnflem3  9728  cantnf  9730  cnfcom3lem  9740  onssr1  9868  rankunb  9887  tcrank  9921  harcard  10015  carduni  10018  infxpenlem  10050  infpwfien  10099  dfac12r  10184  ackbij2lem1  10255  ackbij1lem18  10273  isfin1-3  10423  fin1a2lem11  10447  fin1a2lem13  10449  zorn2lem4  10536  zorn2lem5  10537  ttukeylem6  10551  ttukeylem7  10552  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2  10680  wunr1om  10756  wunom  10757  tskr1om  10804  tskr1om2  10805  tskxpss  10809  tskcard  10818  tskuni  10820  grothomex  10866  genpss  11041  distrlem1pr  11062  distrlem5pr  11064  ltexprlem2  11074  ltexprlem6  11078  ltexprlem7  11079  reclem3pr  11086  reclem4pr  11087  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  peano5uzi  12704  uzss  12898  ixxdisj  13398  ixxss1  13401  ixxss2  13402  ixxss12  13403  ixxub  13404  ixxlb  13405  iocssre  13463  icossre  13464  iccssre  13465  icodisj  13512  fzss1  13599  fzss2  13600  ssfzunsnext  13605  fzosplit  13728  fzouzsplit  13730  ssfzo12bi  13796  ssnn0fi  14022  fsuppmapnn0fiub  14028  suppssfz  14031  sswrd  14556  rtrclreclem3  15095  isercoll  15700  summolem2a  15747  fsumcvg3  15761  fsum2dlem  15802  fsumcom2  15806  qshash  15859  prodmolem2a  15966  fprod2dlem  16012  fprodcom2  16016  bitsfzo  16468  1arith  16960  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  ramtlecl  17033  prmgaplem3  17086  prmgaplem4  17087  monhom  17782  epihom  17789  funcsetcres2  18146  funcestrcsetclem8  18202  funcsetcestrclem8  18217  psdmrn  18630  gsumwspan  18871  frmdss2  18888  sursubmefmnd  18921  injsubmefmnd  18922  trivsubgsnd  19184  ssnmz  19196  trivnsgd  19202  kerf1ghm  19277  conjnmz  19282  symgvalstruct  19428  symgvalstructOLD  19429  gex1  19623  sylow2alem1  19649  lsmless1x  19676  lsmless2x  19677  lsmub1x  19678  lsmub2x  19679  lsmmod  19707  lsmdisj2  19714  efgrelexlemb  19782  efgcpbllemb  19787  cntzcmn  19872  gsum2d2  20006  dprdub  20059  dprdss  20063  dprddisj2  20073  pgpfac1lem3  20111  subrngmre  20578  subrguss  20603  subrgmre  20613  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap2  20674  rhmsscmap  20675  rhmsscrnghm  20681  rngcresringcat  20685  funcringcsetc  20690  unitrrg  20719  isdrng2  20759  primefld0cl  20823  primefld1cl  20824  lssssr  20969  lsssssubg  20973  lssmre  20981  lbspss  21098  lspdisj  21144  lbsextlem2  21178  lidl1el  21253  drngnidl  21270  lpiss  21356  zsssubrg  21460  qsssubdrg  21461  cnsubrg  21462  mulgrhm2  21506  znrrg  21601  ocvocv  21706  ocv2ss  21708  ocvin  21709  lsmcss  21727  cssmre  21728  pjcss  21753  lindfrn  21858  sraassab  21905  mhpsubg  22174  evls1maprnss  22397  dmatsgrp  22520  scmatsgrp  22540  scmatsgrp1  22543  m2cpmrngiso  22779  bastg  22988  tgss  22990  tgtop  22995  tgidm  23002  en2top  23007  neisspw  23130  topssnei  23147  neiptopuni  23153  lpss3  23167  clslp  23171  tgrest  23182  ssrest  23199  restntr  23205  ordtbas2  23214  ordtbas  23215  cnss1  23299  cnss2  23300  cnsscnp  23302  cnrest2r  23310  cmpsublem  23422  cmpsub  23423  tgcmp  23424  cmpcld  23425  hauscmplem  23429  cnconn  23445  llyss  23502  nllyss  23503  restnlly  23505  restlly  23506  locfincmp  23549  locfincf  23554  kgenss  23566  kgenidm  23570  llycmpkgen2  23573  1stckgen  23577  kgen2ss  23578  kgencn3  23581  ptbasfi  23604  ptpjopn  23635  txdis  23655  txkgen  23675  xkoptsub  23677  xkopjcn  23679  txconn  23712  qtoptop2  23722  qtopuni  23725  qtopkgen  23733  basqtop  23734  tgqtop  23735  qtopss  23738  qtoprest  23740  qtopomap  23741  qtopcmap  23742  kqsat  23754  kqcldsat  23756  hmphdis  23819  isfild  23881  ssfg  23895  fgss  23896  fgss2  23897  fgfil  23898  fgabs  23902  filconn  23906  fgtr  23913  uzrest  23920  ufilmax  23930  ufileu  23942  filufint  23943  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  flimss2  23995  flimss1  23996  flimclsi  24001  flimcf  24005  flimsncls  24009  fclssscls  24041  fclsss1  24045  fclsss2  24046  fclscf  24048  uffclsflim  24054  alexsublem  24067  alexsubALTlem3  24072  ptcmplem2  24076  ptcmplem3  24077  cnextf  24089  efmndtmd  24124  symgtgp  24129  cldsubg  24134  tsmscl  24158  haustsms2  24160  tgptsmscls  24173  tsmsxp  24178  restutop  24261  ustuqtop4  24268  utop2nei  24274  utop3cls  24275  ucncn  24309  xblss2ps  24426  xblss2  24427  xrsblre  24846  xrsmopn  24847  recld2  24849  zdis  24851  icccmplem2  24858  cncfss  24938  cnheiborlem  24999  htpycn  25018  phtpyhtpy  25027  pi1blem  25085  cphsscph  25298  cfilfcls  25321  iscmet3lem2  25339  iscmet2  25341  caussi  25344  equivcfil  25346  lmcau  25360  metsscmetcld  25362  hlhil  25490  ivthicc  25506  ovoliunnul  25555  ovolicopnf  25572  uniioombllem3  25633  dyadmbllem  25647  volsup2  25653  vitalilem2  25657  itg1addlem4  25747  itg1addlem4OLD  25748  itg10a  25759  itg1ge0a  25760  mbfi1fseqlem4  25767  itg2gt0  25809  limciun  25943  perfdvf  25952  cpnord  25985  dvcj  26002  dvlip2  26048  dvivth  26063  dvne0  26064  dvcnvre  26072  ply1lpir  26235  plyco0  26245  plyexmo  26369  abelth  26499  efif1o  26602  logno1  26692  efopnlem2  26713  loglesqrt  26818  lgamcvg2  27112  ppisval  27161  ppinprm  27209  chtnprm  27211  fsumvma  27271  dchrfi  27313  chtppilimlem2  27532  chebbnd2  27535  vmadivsumb  27541  rplogsumlem2  27543  dchrisumlem2  27548  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  selbergb  27607  selberg2b  27610  selberg3lem1  27615  selberg3lem2  27616  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  oldssmade  27930  sltlpss  27959  noseqrdgfn  28326  peano5uzs  28404  uhgredgss  29162  usgruspgrb  29214  uhgrissubgr  29306  uhgrspansubgrlem  29321  uhgrspan1  29334  cusgredg  29455  usgredgsscusgredg  29491  ococss  31321  shsub1  31352  shless  31387  shmodsi  31417  pjhth  31421  spansnss  31599  spanpr  31608  spansnm0i  31678  pjjsi  31728  sumdmdii  32443  sumdmdlem  32446  sumdmdlem2  32447  cdj3lem1  32462  abrexss  32539  fnpreimac  32687  rnmposs  32690  unifi3  32729  uzssico  32792  ssnnssfz  32795  pwrssmgc  32974  pmtrcnel  33091  cycpmrn  33145  cyc3evpm  33152  cycpmgcl  33155  elrgspnlem1  33231  elrgspnlem3  33233  elrgspnlem4  33234  fldgensdrg  33295  ringlsmss1  33403  ringlsmss2  33404  prmidlssidl  33452  mxidlirredi  33478  drngmxidl  33484  drngmxidlr  33485  1arithidomlem1  33542  1arithidom  33544  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  ply1mulrtss  33585  dimkerim  33654  extdg1id  33690  irngss  33701  irngssv  33702  algextdeglem8  33729  constrsscn  33744  constrsslem  33745  crefss  33809  cmpcref  33810  zarmxt1  33840  tpr2rico  33872  esumrnmpt2  34048  esumpcvgval  34058  ldsysgenld  34140  sigapildsys  34142  ldgenpisys  34146  cldssbrsiga  34167  measdivcstALTV  34205  mbfmcnt  34249  oddpwdc  34335  eulerpartlemgs2  34361  reprpmtf1o  34619  bnj1033  34961  bnj1398  35026  sconnpi1  35223  cvmscld  35257  cvmliftlem15  35282  satfrnmapom  35354  dfon2lem6  35769  fnessref  36339  fgmin  36352  tailfb  36359  dissneqlem  37322  icoreresf  37334  rdglimss  37359  finxpreclem6  37378  lindsenlbs  37601  poimirlem11  37617  poimirlem12  37618  sstotbnd3  37762  prdstotbnd  37780  cntotbnd  37782  ismtyhmeo  37791  1idl  38012  disjdmqsss  38783  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  41952  dvrelog2  42045  dvrelog3  42046  aks4d1p3  42059  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8  42068  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  hashscontpow1  42102  aks6d1c4  42105  sticksstones3  42129  aks6d1c6lem3  42153  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  rhmqusspan  42166  unitscyglem1  42176  unitscyglem4  42179  ss2ab1  42236  eldiophss  42761  rencldnfilem  42807  pellexlem5  42820  pell14qrss1234  42843  pell1qrss14  42855  pellfundre  42868  pellfundge  42869  pellfundlb  42871  pellfundglb  42872  harinf  43022  proot1hash  43183  safesnsupfiss  43404  intabssd  43508  ss2iundf  43648  ov2ssiunov2  43689  clsk1indlem3  44032  radcnvrat  44309  nznngen  44311  trsspwALT3  44817  sspwimpALT2  44925  refsumcn  44967  iinssf  45077  icoiccdif  45476  icccncfext  45842  stoweidlem27  45982  stoweidlem46  46001  stoweidlem57  46012  fourierdlem40  46102  fourierdlem78  46139  ffnafv  47120  iccpartrn  47354  sprsymrelfvlem  47414  sprsymrelf1lem  47415  clnbgrssedg  47764  stgrusgra  47861  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  ssnn0ssfz  48193  lincolss  48279  lcoss  48281  lcosslsp  48283  iunord  48906