Theorem ssrdv 3988

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2107   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  eqelssd  4003  ss2abdvALT  4061  sscon  4138  ssdif  4139  unss1  4179  ssrin  4233  eq0rdvALT  4405  sspw  4613  elpwdifsn  4792  uniss  4916  intss1  4967  intmin  4972  intssuni  4974  iinssiun  5010  iunss1  5011  iinss1  5012  ss2iun  5015  ssiun  5049  ssiun2  5050  iinss  5059  iinss2  5060  iunxdif3  5098  sspwb  5449  pwssun  5571  relop  5849  dmss  5901  dmcosseq  5971  ssrnres  6175  sossfld  6183  predtrss  6321  preddowncl  6331  tron  6385  tz7.7  6388  funimassd  6956  dffv2  6984  chfnrn  7048  fvn0ssdmfun  7074  fveqdmss  7078  dff3  7099  ffnfv  7115  f1imass  7260  ssorduni  7763  onint  7775  limsssuc  7836  limuni3  7838  limomss  7857  fo1stres  7998  fo2ndres  7999  fo2ndf  8104  fnse  8116  ressuppssdif  8167  suppss  8176  suppssOLD  8177  reldmtpos  8216  fprlem2  8283  onfununi  8338  smoiun  8358  smocdmdom  8365  tz7.48-1  8440  tz7.49  8442  oaass  8558  cofon1  8668  cofon2  8669  qsss  8769  uniinqs  8788  pmss12g  8860  mapss  8880  ixpssmap2g  8918  ixpssmapg  8919  pssnn  9165  fineqv  9260  pssnnOLD  9262  ssfii  9411  dffi2  9415  oismo  9532  unxpwdom2  9580  inf3lemd  9619  inf3lem1  9620  inf3lem6  9625  cantnflem3  9683  cantnf  9685  cnfcom3lem  9695  onssr1  9823  rankunb  9842  tcrank  9876  harcard  9970  carduni  9973  infxpenlem  10005  infpwfien  10054  dfac12r  10138  ackbij2lem1  10211  ackbij1lem18  10229  isfin1-3  10378  fin1a2lem11  10402  fin1a2lem13  10404  zorn2lem4  10491  zorn2lem5  10492  ttukeylem6  10506  ttukeylem7  10507  fpwwe2lem10  10632  fpwwe2lem11  10633  fpwwe2  10635  wunr1om  10711  wunom  10712  tskr1om  10759  tskr1om2  10760  tskxpss  10764  tskcard  10773  tskuni  10775  grothomex  10821  genpss  10996  distrlem1pr  11017  distrlem5pr  11019  ltexprlem2  11029  ltexprlem6  11033  ltexprlem7  11034  reclem3pr  11041  reclem4pr  11042  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  peano5uzi  12648  uzss  12842  ixxdisj  13336  ixxss1  13339  ixxss2  13340  ixxss12  13341  ixxub  13342  ixxlb  13343  iocssre  13401  icossre  13402  iccssre  13403  icodisj  13450  fzss1  13537  fzss2  13538  ssfzunsnext  13543  fzosplit  13662  fzouzsplit  13664  ssfzo12bi  13724  ssnn0fi  13947  fsuppmapnn0fiub  13953  suppssfz  13956  sswrd  14469  rtrclreclem3  15004  isercoll  15611  summolem2a  15658  fsumcvg3  15672  fsum2dlem  15713  fsumcom2  15717  qshash  15770  prodmolem2a  15875  fprod2dlem  15921  fprodcom2  15925  bitsfzo  16373  1arith  16857  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  ramtlecl  16930  prmgaplem3  16983  prmgaplem4  16984  monhom  17679  epihom  17686  funcsetcres2  18040  funcestrcsetclem8  18096  funcsetcestrclem8  18111  psdmrn  18523  gsumwspan  18724  frmdss2  18741  sursubmefmnd  18774  injsubmefmnd  18775  trivsubgsnd  19029  ssnmz  19041  trivnsgd  19047  conjnmz  19121  symgvalstruct  19259  symgvalstructOLD  19260  gex1  19454  sylow2alem1  19480  lsmless1x  19507  lsmless2x  19508  lsmub1x  19509  lsmub2x  19510  lsmmod  19538  lsmdisj2  19545  efgrelexlemb  19613  efgcpbllemb  19618  cntzcmn  19703  gsum2d2  19837  dprdub  19890  dprdss  19894  dprddisj2  19904  pgpfac1lem3  19942  kerf1ghm  20275  isdrng2  20322  subrguss  20371  subrgmre  20381  primefld0cl  20415  primefld1cl  20416  lssssr  20557  lsssssubg  20562  lssmre  20570  lbspss  20686  lspdisj  20731  lbsextlem2  20765  lidl1el  20834  drngnidl  20847  lpiss  20881  unitrrg  20902  zsssubrg  20996  qsssubdrg  20997  cnsubrg  20998  mulgrhm2  21040  znrrg  21113  ocvocv  21216  ocv2ss  21218  ocvin  21219  lsmcss  21237  cssmre  21238  pjcss  21263  lindfrn  21368  sraassab  21414  mhpsubg  21688  dmatsgrp  21993  scmatsgrp  22013  scmatsgrp1  22016  m2cpmrngiso  22252  bastg  22461  tgss  22463  tgtop  22468  tgidm  22475  en2top  22480  neisspw  22603  topssnei  22620  neiptopuni  22626  lpss3  22640  clslp  22644  tgrest  22655  ssrest  22672  restntr  22678  ordtbas2  22687  ordtbas  22688  cnss1  22772  cnss2  22773  cnsscnp  22775  cnrest2r  22783  cmpsublem  22895  cmpsub  22896  tgcmp  22897  cmpcld  22898  hauscmplem  22902  cnconn  22918  llyss  22975  nllyss  22976  restnlly  22978  restlly  22979  locfincmp  23022  locfincf  23027  kgenss  23039  kgenidm  23043  llycmpkgen2  23046  1stckgen  23050  kgen2ss  23051  kgencn3  23054  ptbasfi  23077  ptpjopn  23108  txdis  23128  txkgen  23148  xkoptsub  23150  xkopjcn  23152  txconn  23185  qtoptop2  23195  qtopuni  23198  qtopkgen  23206  basqtop  23207  tgqtop  23208  qtopss  23211  qtoprest  23213  qtopomap  23214  qtopcmap  23215  kqsat  23227  kqcldsat  23229  hmphdis  23292  isfild  23354  ssfg  23368  fgss  23369  fgss2  23370  fgfil  23371  fgabs  23375  filconn  23379  fgtr  23386  uzrest  23393  ufilmax  23403  ufileu  23415  filufint  23416  rnelfm  23449  fmfnfmlem2  23451  fmfnfmlem4  23453  flimss2  23468  flimss1  23469  flimclsi  23474  flimcf  23478  flimsncls  23482  fclssscls  23514  fclsss1  23518  fclsss2  23519  fclscf  23521  uffclsflim  23527  alexsublem  23540  alexsubALTlem3  23545  ptcmplem2  23549  ptcmplem3  23550  cnextf  23562  efmndtmd  23597  symgtgp  23602  cldsubg  23607  tsmscl  23631  haustsms2  23633  tgptsmscls  23646  tsmsxp  23651  restutop  23734  ustuqtop4  23741  utop2nei  23747  utop3cls  23748  ucncn  23782  xblss2ps  23899  xblss2  23900  xrsblre  24319  xrsmopn  24320  recld2  24322  zdis  24324  icccmplem2  24331  cncfss  24407  cnheiborlem  24462  htpycn  24481  phtpyhtpy  24490  pi1blem  24547  cphsscph  24760  cfilfcls  24783  iscmet3lem2  24801  iscmet2  24803  caussi  24806  equivcfil  24808  lmcau  24822  metsscmetcld  24824  hlhil  24952  ivthicc  24967  ovoliunnul  25016  ovolicopnf  25033  uniioombllem3  25094  dyadmbllem  25108  volsup2  25114  vitalilem2  25118  itg1addlem4  25208  itg1addlem4OLD  25209  itg10a  25220  itg1ge0a  25221  mbfi1fseqlem4  25228  itg2gt0  25270  limciun  25403  perfdvf  25412  cpnord  25444  dvcj  25459  dvlip2  25504  dvivth  25519  dvne0  25520  dvcnvre  25528  ply1lpir  25688  plyco0  25698  plyexmo  25818  abelth  25945  efif1o  26047  logno1  26136  efopnlem2  26157  loglesqrt  26256  lgamcvg2  26549  ppisval  26598  ppinprm  26646  chtnprm  26648  fsumvma  26706  dchrfi  26748  chtppilimlem2  26967  chebbnd2  26970  vmadivsumb  26976  rplogsumlem2  26978  dchrisumlem2  26983  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  selbergb  27042  selberg2b  27045  selberg3lem1  27050  selberg3lem2  27051  selberg3  27052  selberg4lem1  27053  selberg4  27054  pntrlog2bndlem2  27071  pntrlog2bndlem4  27073  oldssmade  27362  sltlpss  27391  uhgredgss  28381  usgruspgrb  28431  uhgrissubgr  28522  uhgrspansubgrlem  28537  uhgrspan1  28550  cusgredg  28671  usgredgsscusgredg  28706  ococss  30534  shsub1  30565  shless  30600  shmodsi  30630  pjhth  30634  spansnss  30812  spanpr  30821  spansnm0i  30891  pjjsi  30941  sumdmdii  31656  sumdmdlem  31659  sumdmdlem2  31660  cdj3lem1  31675  abrexss  31737  fnpreimac  31884  rnmposs  31887  unifi3  31925  uzssico  31983  ssnnssfz  31986  pwrssmgc  32158  pmtrcnel  32238  cycpmrn  32290  cyc3evpm  32297  cycpmgcl  32300  fldgensdrg  32393  ringlsmss1  32495  ringlsmss2  32496  prmidlssidl  32552  mxidlirredi  32576  drngmxidl  32582  dimkerim  32701  extdg1id  32731  irngss  32740  irngssv  32741  evls1maprnss  32750  crefss  32818  cmpcref  32819  zarmxt1  32849  tpr2rico  32881  esumrnmpt2  33055  esumpcvgval  33065  ldsysgenld  33147  sigapildsys  33149  ldgenpisys  33153  cldssbrsiga  33174  measdivcstALTV  33212  mbfmcnt  33256  oddpwdc  33342  eulerpartlemgs2  33368  reprpmtf1o  33627  bnj1033  33969  bnj1398  34034  sconnpi1  34219  cvmscld  34253  cvmliftlem15  34278  satfrnmapom  34350  dfon2lem6  34749  fnessref  35231  fgmin  35244  tailfb  35251  dissneqlem  36210  icoreresf  36222  rdglimss  36247  finxpreclem6  36266  lindsenlbs  36472  poimirlem11  36488  poimirlem12  36489  sstotbnd3  36633  prdstotbnd  36651  cntotbnd  36653  ismtyhmeo  36662  1idl  36883  disjdmqsss  37661  lshpdisj  37846  lssats  37871  lkrin  38023  glbconxN  38238  paddss1  38677  paddss2  38678  paddasslem16  38695  paddidm  38701  pmodlem2  38707  pmapjoin  38712  pmapjat1  38713  pclfinN  38760  pclfinclN  38810  diasslssN  39919  dia2dimlem12  39935  dihsslss  40136  baerlem3lem2  40570  baerlem5alem2  40571  baerlem5blem2  40572  dvrelog2  40918  dvrelog3  40919  aks4d1p3  40932  aks4d1p4  40933  aks4d1p5  40934  aks4d1p7  40937  aks4d1p8  40941  sticksstones3  40953  ss2ab1  41033  eldiophss  41498  rencldnfilem  41544  pellexlem5  41557  pell14qrss1234  41580  pell1qrss14  41592  pellfundre  41605  pellfundge  41606  pellfundlb  41608  pellfundglb  41609  harinf  41759  proot1hash  41928  safesnsupfiss  42152  intabssd  42256  ss2iundf  42396  ov2ssiunov2  42437  clsk1indlem3  42780  finnzfsuppd  42947  radcnvrat  43059  nznngen  43061  trsspwALT3  43567  sspwimpALT2  43675  refsumcn  43700  iinssf  43813  icoiccdif  44224  icccncfext  44590  stoweidlem27  44730  stoweidlem46  44749  stoweidlem57  44760  fourierdlem40  44850  fourierdlem78  44887  ffnafv  45866  iccpartrn  46085  sprsymrelfvlem  46145  sprsymrelf1lem  46146  subrngmre  46726  rnghmsscmap2  46825  rnghmsscmap  46826  funcrngcsetc  46850  funcrngcsetcALT  46851  rhmsscmap2  46871  rhmsscmap  46872  rhmsscrnghm  46878  rngcresringcat  46882  funcringcsetc  46887  funcringcsetcALTV2lem8  46895  funcringcsetclem8ALTV  46918  rhmsubcALTVlem4  46959  ssnn0ssfz  46979  lincolss  47069  lcoss  47071  lcosslsp  47073  iunord  47675