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

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

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 3956  df-ss 3966

This theorem is referenced by:  eqelssd  4004  ss2abdvALT  4062  sscon  4139  ssdif  4140  unss1  4180  ssrin  4234  eq0rdvALT  4406  sspw  4614  elpwdifsn  4793  uniss  4917  intss1  4968  intmin  4973  intssuni  4975  iinssiun  5011  iunss1  5012  iinss1  5013  ss2iun  5016  ssiun  5050  ssiun2  5051  iinss  5060  iinss2  5061  iunxdif3  5099  sspwb  5450  pwssun  5572  relop  5851  dmss  5903  dmcosseq  5973  ssrnres  6178  sossfld  6186  predtrss  6324  preddowncl  6334  tron  6388  tz7.7  6391  funimassd  6959  dffv2  6987  chfnrn  7051  fvn0ssdmfun  7077  fveqdmss  7081  dff3  7102  ffnfv  7118  f1imass  7263  ssorduni  7766  onint  7778  limsssuc  7839  limuni3  7841  limomss  7860  fo1stres  8001  fo2ndres  8002  fo2ndf  8107  fnse  8119  ressuppssdif  8170  suppss  8179  suppssOLD  8180  reldmtpos  8219  fprlem2  8286  onfununi  8341  smoiun  8361  smocdmdom  8368  tz7.48-1  8443  tz7.49  8445  oaass  8561  cofon1  8671  cofon2  8672  qsss  8772  uniinqs  8791  pmss12g  8863  mapss  8883  ixpssmap2g  8921  ixpssmapg  8922  pssnn  9168  fineqv  9263  pssnnOLD  9265  ssfii  9414  dffi2  9418  oismo  9535  unxpwdom2  9583  inf3lemd  9622  inf3lem1  9623  inf3lem6  9628  cantnflem3  9686  cantnf  9688  cnfcom3lem  9698  onssr1  9826  rankunb  9845  tcrank  9879  harcard  9973  carduni  9976  infxpenlem  10008  infpwfien  10057  dfac12r  10141  ackbij2lem1  10214  ackbij1lem18  10232  isfin1-3  10381  fin1a2lem11  10405  fin1a2lem13  10407  zorn2lem4  10494  zorn2lem5  10495  ttukeylem6  10509  ttukeylem7  10510  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2  10638  wunr1om  10714  wunom  10715  tskr1om  10762  tskr1om2  10763  tskxpss  10767  tskcard  10776  tskuni  10778  grothomex  10824  genpss  10999  distrlem1pr  11020  distrlem5pr  11022  ltexprlem2  11032  ltexprlem6  11036  ltexprlem7  11037  reclem3pr  11044  reclem4pr  11045  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  peano5uzi  12651  uzss  12845  ixxdisj  13339  ixxss1  13342  ixxss2  13343  ixxss12  13344  ixxub  13345  ixxlb  13346  iocssre  13404  icossre  13405  iccssre  13406  icodisj  13453  fzss1  13540  fzss2  13541  ssfzunsnext  13546  fzosplit  13665  fzouzsplit  13667  ssfzo12bi  13727  ssnn0fi  13950  fsuppmapnn0fiub  13956  suppssfz  13959  sswrd  14472  rtrclreclem3  15007  isercoll  15614  summolem2a  15661  fsumcvg3  15675  fsum2dlem  15716  fsumcom2  15720  qshash  15773  prodmolem2a  15878  fprod2dlem  15924  fprodcom2  15928  bitsfzo  16376  1arith  16860  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  ramtlecl  16933  prmgaplem3  16986  prmgaplem4  16987  monhom  17682  epihom  17689  funcsetcres2  18043  funcestrcsetclem8  18099  funcsetcestrclem8  18114  psdmrn  18526  gsumwspan  18727  frmdss2  18744  sursubmefmnd  18777  injsubmefmnd  18778  trivsubgsnd  19034  ssnmz  19046  trivnsgd  19052  conjnmz  19126  symgvalstruct  19264  symgvalstructOLD  19265  gex1  19459  sylow2alem1  19485  lsmless1x  19512  lsmless2x  19513  lsmub1x  19514  lsmub2x  19515  lsmmod  19543  lsmdisj2  19550  efgrelexlemb  19618  efgcpbllemb  19623  cntzcmn  19708  gsum2d2  19842  dprdub  19895  dprdss  19899  dprddisj2  19909  pgpfac1lem3  19947  kerf1ghm  20282  subrguss  20334  subrgmre  20344  isdrng2  20371  primefld0cl  20422  primefld1cl  20423  lssssr  20564  lsssssubg  20569  lssmre  20577  lbspss  20693  lspdisj  20738  lbsextlem2  20772  lidl1el  20841  drngnidl  20854  lpiss  20888  unitrrg  20909  zsssubrg  21003  qsssubdrg  21004  cnsubrg  21005  mulgrhm2  21048  znrrg  21121  ocvocv  21224  ocv2ss  21226  ocvin  21227  lsmcss  21245  cssmre  21246  pjcss  21271  lindfrn  21376  sraassab  21422  mhpsubg  21696  dmatsgrp  22001  scmatsgrp  22021  scmatsgrp1  22024  m2cpmrngiso  22260  bastg  22469  tgss  22471  tgtop  22476  tgidm  22483  en2top  22488  neisspw  22611  topssnei  22628  neiptopuni  22634  lpss3  22648  clslp  22652  tgrest  22663  ssrest  22680  restntr  22686  ordtbas2  22695  ordtbas  22696  cnss1  22780  cnss2  22781  cnsscnp  22783  cnrest2r  22791  cmpsublem  22903  cmpsub  22904  tgcmp  22905  cmpcld  22906  hauscmplem  22910  cnconn  22926  llyss  22983  nllyss  22984  restnlly  22986  restlly  22987  locfincmp  23030  locfincf  23035  kgenss  23047  kgenidm  23051  llycmpkgen2  23054  1stckgen  23058  kgen2ss  23059  kgencn3  23062  ptbasfi  23085  ptpjopn  23116  txdis  23136  txkgen  23156  xkoptsub  23158  xkopjcn  23160  txconn  23193  qtoptop2  23203  qtopuni  23206  qtopkgen  23214  basqtop  23215  tgqtop  23216  qtopss  23219  qtoprest  23221  qtopomap  23222  qtopcmap  23223  kqsat  23235  kqcldsat  23237  hmphdis  23300  isfild  23362  ssfg  23376  fgss  23377  fgss2  23378  fgfil  23379  fgabs  23383  filconn  23387  fgtr  23394  uzrest  23401  ufilmax  23411  ufileu  23423  filufint  23424  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  flimss2  23476  flimss1  23477  flimclsi  23482  flimcf  23486  flimsncls  23490  fclssscls  23522  fclsss1  23526  fclsss2  23527  fclscf  23529  uffclsflim  23535  alexsublem  23548  alexsubALTlem3  23553  ptcmplem2  23557  ptcmplem3  23558  cnextf  23570  efmndtmd  23605  symgtgp  23610  cldsubg  23615  tsmscl  23639  haustsms2  23641  tgptsmscls  23654  tsmsxp  23659  restutop  23742  ustuqtop4  23749  utop2nei  23755  utop3cls  23756  ucncn  23790  xblss2ps  23907  xblss2  23908  xrsblre  24327  xrsmopn  24328  recld2  24330  zdis  24332  icccmplem2  24339  cncfss  24415  cnheiborlem  24470  htpycn  24489  phtpyhtpy  24498  pi1blem  24555  cphsscph  24768  cfilfcls  24791  iscmet3lem2  24809  iscmet2  24811  caussi  24814  equivcfil  24816  lmcau  24830  metsscmetcld  24832  hlhil  24960  ivthicc  24975  ovoliunnul  25024  ovolicopnf  25041  uniioombllem3  25102  dyadmbllem  25116  volsup2  25122  vitalilem2  25126  itg1addlem4  25216  itg1addlem4OLD  25217  itg10a  25228  itg1ge0a  25229  mbfi1fseqlem4  25236  itg2gt0  25278  limciun  25411  perfdvf  25420  cpnord  25452  dvcj  25467  dvlip2  25512  dvivth  25527  dvne0  25528  dvcnvre  25536  ply1lpir  25696  plyco0  25706  plyexmo  25826  abelth  25953  efif1o  26055  logno1  26144  efopnlem2  26165  loglesqrt  26266  lgamcvg2  26559  ppisval  26608  ppinprm  26656  chtnprm  26658  fsumvma  26716  dchrfi  26758  chtppilimlem2  26977  chebbnd2  26980  vmadivsumb  26986  rplogsumlem2  26988  dchrisumlem2  26993  vmalogdivsum2  27041  vmalogdivsum  27042  2vmadivsumlem  27043  selbergb  27052  selberg2b  27055  selberg3lem1  27060  selberg3lem2  27061  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  oldssmade  27372  sltlpss  27401  uhgredgss  28391  usgruspgrb  28441  uhgrissubgr  28532  uhgrspansubgrlem  28547  uhgrspan1  28560  cusgredg  28681  usgredgsscusgredg  28716  ococss  30546  shsub1  30577  shless  30612  shmodsi  30642  pjhth  30646  spansnss  30824  spanpr  30833  spansnm0i  30903  pjjsi  30953  sumdmdii  31668  sumdmdlem  31671  sumdmdlem2  31672  cdj3lem1  31687  abrexss  31749  fnpreimac  31896  rnmposs  31899  unifi3  31937  uzssico  31995  ssnnssfz  31998  pwrssmgc  32170  pmtrcnel  32250  cycpmrn  32302  cyc3evpm  32309  cycpmgcl  32312  fldgensdrg  32404  ringlsmss1  32506  ringlsmss2  32507  prmidlssidl  32563  mxidlirredi  32587  drngmxidl  32593  dimkerim  32712  extdg1id  32742  irngss  32751  irngssv  32752  evls1maprnss  32761  crefss  32829  cmpcref  32830  zarmxt1  32860  tpr2rico  32892  esumrnmpt2  33066  esumpcvgval  33076  ldsysgenld  33158  sigapildsys  33160  ldgenpisys  33164  cldssbrsiga  33185  measdivcstALTV  33223  mbfmcnt  33267  oddpwdc  33353  eulerpartlemgs2  33379  reprpmtf1o  33638  bnj1033  33980  bnj1398  34045  sconnpi1  34230  cvmscld  34264  cvmliftlem15  34289  satfrnmapom  34361  dfon2lem6  34760  fnessref  35242  fgmin  35255  tailfb  35262  dissneqlem  36221  icoreresf  36233  rdglimss  36258  finxpreclem6  36277  lindsenlbs  36483  poimirlem11  36499  poimirlem12  36500  sstotbnd3  36644  prdstotbnd  36662  cntotbnd  36664  ismtyhmeo  36673  1idl  36894  disjdmqsss  37672  lshpdisj  37857  lssats  37882  lkrin  38034  glbconxN  38249  paddss1  38688  paddss2  38689  paddasslem16  38706  paddidm  38712  pmodlem2  38718  pmapjoin  38723  pmapjat1  38724  pclfinN  38771  pclfinclN  38821  diasslssN  39930  dia2dimlem12  39946  dihsslss  40147  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  dvrelog2  40929  dvrelog3  40930  aks4d1p3  40943  aks4d1p4  40944  aks4d1p5  40945  aks4d1p7  40948  aks4d1p8  40952  sticksstones3  40964  ss2ab1  41036  eldiophss  41512  rencldnfilem  41558  pellexlem5  41571  pell14qrss1234  41594  pell1qrss14  41606  pellfundre  41619  pellfundge  41620  pellfundlb  41622  pellfundglb  41623  harinf  41773  proot1hash  41942  safesnsupfiss  42166  intabssd  42270  ss2iundf  42410  ov2ssiunov2  42451  clsk1indlem3  42794  finnzfsuppd  42961  radcnvrat  43073  nznngen  43075  trsspwALT3  43581  sspwimpALT2  43689  refsumcn  43714  iinssf  43827  icoiccdif  44237  icccncfext  44603  stoweidlem27  44743  stoweidlem46  44762  stoweidlem57  44773  fourierdlem40  44863  fourierdlem78  44900  ffnafv  45879  iccpartrn  46098  sprsymrelfvlem  46158  sprsymrelf1lem  46159  subrngmre  46741  rnghmsscmap2  46871  rnghmsscmap  46872  funcrngcsetc  46896  funcrngcsetcALT  46897  rhmsscmap2  46917  rhmsscmap  46918  rhmsscrnghm  46924  rngcresringcat  46928  funcringcsetc  46933  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  rhmsubcALTVlem4  47005  ssnn0ssfz  47025  lincolss  47115  lcoss  47117  lcosslsp  47119  iunord  47721