Theorem ssrdv 3986

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

Syntax hints:   → wi 4  ∀wal 1532   ∈ wcel 2099   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  eqelssd  4001  ss2abdvALT  4059  sscon  4137  ssdif  4138  unss1  4179  ssrin  4234  eq0rdvALT  4406  sspw  4614  elpwdifsn  4793  uniss  4916  intss1  4966  intmin  4971  intssuni  4973  iinssiun  5009  iunss1  5010  iinss1  5011  ss2iun  5014  ssiun  5049  ssiun2  5050  iinss  5059  iinss2  5060  iunxdif3  5098  sspwb  5451  pwssun  5573  relop  5853  dmss  5905  dmcosseq  5976  ssrnres  6182  sossfld  6190  predtrss  6328  preddowncl  6338  tron  6392  tz7.7  6395  funimassd  6965  dffv2  6993  chfnrn  7058  fvn0ssdmfun  7084  fveqdmss  7088  dff3  7110  ffnfv  7129  f1imass  7274  ssorduni  7781  onint  7793  limsssuc  7854  limuni3  7856  limomss  7875  fo1stres  8019  fo2ndres  8020  fo2ndf  8126  fnse  8138  ressuppssdif  8190  suppss  8199  suppssOLD  8200  reldmtpos  8240  fprlem2  8307  onfununi  8362  smoiun  8382  smocdmdom  8389  tz7.48-1  8464  tz7.49  8466  oaass  8582  cofon1  8693  cofon2  8694  qsss  8797  uniinqs  8816  pmss12g  8888  mapss  8908  ixpssmap2g  8946  ixpssmapg  8947  pssnn  9193  fineqv  9288  pssnnOLD  9290  ssfii  9443  dffi2  9447  oismo  9564  unxpwdom2  9612  inf3lemd  9651  inf3lem1  9652  inf3lem6  9657  cantnflem3  9715  cantnf  9717  cnfcom3lem  9727  onssr1  9855  rankunb  9874  tcrank  9908  harcard  10002  carduni  10005  infxpenlem  10037  infpwfien  10086  dfac12r  10170  ackbij2lem1  10243  ackbij1lem18  10261  isfin1-3  10410  fin1a2lem11  10434  fin1a2lem13  10436  zorn2lem4  10523  zorn2lem5  10524  ttukeylem6  10538  ttukeylem7  10539  fpwwe2lem10  10664  fpwwe2lem11  10665  fpwwe2  10667  wunr1om  10743  wunom  10744  tskr1om  10791  tskr1om2  10792  tskxpss  10796  tskcard  10805  tskuni  10807  grothomex  10853  genpss  11028  distrlem1pr  11049  distrlem5pr  11051  ltexprlem2  11061  ltexprlem6  11065  ltexprlem7  11066  reclem3pr  11073  reclem4pr  11074  supaddc  12212  supadd  12213  supmul1  12214  supmullem2  12216  peano5uzi  12682  uzss  12876  ixxdisj  13372  ixxss1  13375  ixxss2  13376  ixxss12  13377  ixxub  13378  ixxlb  13379  iocssre  13437  icossre  13438  iccssre  13439  icodisj  13486  fzss1  13573  fzss2  13574  ssfzunsnext  13579  fzosplit  13698  fzouzsplit  13700  ssfzo12bi  13760  ssnn0fi  13983  fsuppmapnn0fiub  13989  suppssfz  13992  sswrd  14505  rtrclreclem3  15040  isercoll  15647  summolem2a  15694  fsumcvg3  15708  fsum2dlem  15749  fsumcom2  15753  qshash  15806  prodmolem2a  15911  fprod2dlem  15957  fprodcom2  15961  bitsfzo  16410  1arith  16896  vdwlem2  16951  vdwlem6  16955  vdwlem8  16957  ramtlecl  16969  prmgaplem3  17022  prmgaplem4  17023  monhom  17718  epihom  17725  funcsetcres2  18082  funcestrcsetclem8  18138  funcsetcestrclem8  18153  psdmrn  18565  gsumwspan  18798  frmdss2  18815  sursubmefmnd  18848  injsubmefmnd  18849  trivsubgsnd  19109  ssnmz  19121  trivnsgd  19127  kerf1ghm  19201  conjnmz  19206  symgvalstruct  19351  symgvalstructOLD  19352  gex1  19546  sylow2alem1  19572  lsmless1x  19599  lsmless2x  19600  lsmub1x  19601  lsmub2x  19602  lsmmod  19630  lsmdisj2  19637  efgrelexlemb  19705  efgcpbllemb  19710  cntzcmn  19795  gsum2d2  19929  dprdub  19982  dprdss  19986  dprddisj2  19996  pgpfac1lem3  20034  subrngmre  20499  subrguss  20526  subrgmre  20536  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  rngcresringcat  20602  funcringcsetc  20607  isdrng2  20638  primefld0cl  20694  primefld1cl  20695  lssssr  20838  lsssssubg  20842  lssmre  20850  lbspss  20967  lspdisj  21013  lbsextlem2  21047  lidl1el  21122  drngnidl  21138  lpiss  21219  unitrrg  21240  zsssubrg  21358  qsssubdrg  21359  cnsubrg  21360  mulgrhm2  21404  znrrg  21499  ocvocv  21603  ocv2ss  21605  ocvin  21606  lsmcss  21624  cssmre  21625  pjcss  21650  lindfrn  21755  sraassab  21801  mhpsubg  22077  evls1maprnss  22297  dmatsgrp  22414  scmatsgrp  22434  scmatsgrp1  22437  m2cpmrngiso  22673  bastg  22882  tgss  22884  tgtop  22889  tgidm  22896  en2top  22901  neisspw  23024  topssnei  23041  neiptopuni  23047  lpss3  23061  clslp  23065  tgrest  23076  ssrest  23093  restntr  23099  ordtbas2  23108  ordtbas  23109  cnss1  23193  cnss2  23194  cnsscnp  23196  cnrest2r  23204  cmpsublem  23316  cmpsub  23317  tgcmp  23318  cmpcld  23319  hauscmplem  23323  cnconn  23339  llyss  23396  nllyss  23397  restnlly  23399  restlly  23400  locfincmp  23443  locfincf  23448  kgenss  23460  kgenidm  23464  llycmpkgen2  23467  1stckgen  23471  kgen2ss  23472  kgencn3  23475  ptbasfi  23498  ptpjopn  23529  txdis  23549  txkgen  23569  xkoptsub  23571  xkopjcn  23573  txconn  23606  qtoptop2  23616  qtopuni  23619  qtopkgen  23627  basqtop  23628  tgqtop  23629  qtopss  23632  qtoprest  23634  qtopomap  23635  qtopcmap  23636  kqsat  23648  kqcldsat  23650  hmphdis  23713  isfild  23775  ssfg  23789  fgss  23790  fgss2  23791  fgfil  23792  fgabs  23796  filconn  23800  fgtr  23807  uzrest  23814  ufilmax  23824  ufileu  23836  filufint  23837  rnelfm  23870  fmfnfmlem2  23872  fmfnfmlem4  23874  flimss2  23889  flimss1  23890  flimclsi  23895  flimcf  23899  flimsncls  23903  fclssscls  23935  fclsss1  23939  fclsss2  23940  fclscf  23942  uffclsflim  23948  alexsublem  23961  alexsubALTlem3  23966  ptcmplem2  23970  ptcmplem3  23971  cnextf  23983  efmndtmd  24018  symgtgp  24023  cldsubg  24028  tsmscl  24052  haustsms2  24054  tgptsmscls  24067  tsmsxp  24072  restutop  24155  ustuqtop4  24162  utop2nei  24168  utop3cls  24169  ucncn  24203  xblss2ps  24320  xblss2  24321  xrsblre  24740  xrsmopn  24741  recld2  24743  zdis  24745  icccmplem2  24752  cncfss  24832  cnheiborlem  24893  htpycn  24912  phtpyhtpy  24921  pi1blem  24979  cphsscph  25192  cfilfcls  25215  iscmet3lem2  25233  iscmet2  25235  caussi  25238  equivcfil  25240  lmcau  25254  metsscmetcld  25256  hlhil  25384  ivthicc  25400  ovoliunnul  25449  ovolicopnf  25466  uniioombllem3  25527  dyadmbllem  25541  volsup2  25547  vitalilem2  25551  itg1addlem4  25641  itg1addlem4OLD  25642  itg10a  25653  itg1ge0a  25654  mbfi1fseqlem4  25661  itg2gt0  25703  limciun  25836  perfdvf  25845  cpnord  25878  dvcj  25895  dvlip2  25941  dvivth  25956  dvne0  25957  dvcnvre  25965  ply1lpir  26129  plyco0  26139  plyexmo  26261  abelth  26391  efif1o  26493  logno1  26583  efopnlem2  26604  loglesqrt  26706  lgamcvg2  27000  ppisval  27049  ppinprm  27097  chtnprm  27099  fsumvma  27159  dchrfi  27201  chtppilimlem2  27420  chebbnd2  27423  vmadivsumb  27429  rplogsumlem2  27431  dchrisumlem2  27436  vmalogdivsum2  27484  vmalogdivsum  27485  2vmadivsumlem  27486  selbergb  27495  selberg2b  27498  selberg3lem1  27503  selberg3lem2  27504  selberg3  27505  selberg4lem1  27506  selberg4  27507  pntrlog2bndlem2  27524  pntrlog2bndlem4  27526  oldssmade  27817  sltlpss  27846  noseqrdgfn  28192  uhgredgss  28957  usgruspgrb  29009  uhgrissubgr  29101  uhgrspansubgrlem  29116  uhgrspan1  29129  cusgredg  29250  usgredgsscusgredg  29286  ococss  31116  shsub1  31147  shless  31182  shmodsi  31212  pjhth  31216  spansnss  31394  spanpr  31403  spansnm0i  31473  pjjsi  31523  sumdmdii  32238  sumdmdlem  32241  sumdmdlem2  32242  cdj3lem1  32257  abrexss  32320  fnpreimac  32470  rnmposs  32473  unifi3  32507  uzssico  32565  ssnnssfz  32568  pwrssmgc  32740  pmtrcnel  32825  cycpmrn  32877  cyc3evpm  32884  cycpmgcl  32887  fldgensdrg  33014  ringlsmss1  33118  ringlsmss2  33119  prmidlssidl  33174  mxidlirredi  33197  drngmxidl  33203  dimkerim  33325  extdg1id  33355  irngss  33365  irngssv  33366  algextdeglem8  33392  crefss  33450  cmpcref  33451  zarmxt1  33481  tpr2rico  33513  esumrnmpt2  33687  esumpcvgval  33697  ldsysgenld  33779  sigapildsys  33781  ldgenpisys  33785  cldssbrsiga  33806  measdivcstALTV  33844  mbfmcnt  33888  oddpwdc  33974  eulerpartlemgs2  34000  reprpmtf1o  34258  bnj1033  34600  bnj1398  34665  sconnpi1  34849  cvmscld  34883  cvmliftlem15  34908  satfrnmapom  34980  dfon2lem6  35384  fnessref  35841  fgmin  35854  tailfb  35861  dissneqlem  36819  icoreresf  36831  rdglimss  36856  finxpreclem6  36875  lindsenlbs  37088  poimirlem11  37104  poimirlem12  37105  sstotbnd3  37249  prdstotbnd  37267  cntotbnd  37269  ismtyhmeo  37278  1idl  37499  disjdmqsss  38274  lshpdisj  38459  lssats  38484  lkrin  38636  glbconxN  38851  paddss1  39290  paddss2  39291  paddasslem16  39308  paddidm  39314  pmodlem2  39320  pmapjoin  39325  pmapjat1  39326  pclfinN  39373  pclfinclN  39423  diasslssN  40532  dia2dimlem12  40548  dihsslss  40749  baerlem3lem2  41183  baerlem5alem2  41184  baerlem5blem2  41185  dvrelog2  41535  dvrelog3  41536  aks4d1p3  41549  aks4d1p4  41550  aks4d1p5  41551  aks4d1p7  41554  aks4d1p8  41558  primrootsunit1  41567  primrootscoprmpow  41570  primrootscoprbij  41573  hashscontpow1  41592  aks6d1c4  41595  sticksstones3  41620  aks6d1c6lem3  41644  aks6d1c6isolem2  41647  aks6d1c6lem5  41649  ss2ab1  41707  eldiophss  42194  rencldnfilem  42240  pellexlem5  42253  pell14qrss1234  42276  pell1qrss14  42288  pellfundre  42301  pellfundge  42302  pellfundlb  42304  pellfundglb  42305  harinf  42455  proot1hash  42623  safesnsupfiss  42845  intabssd  42949  ss2iundf  43089  ov2ssiunov2  43130  clsk1indlem3  43473  finnzfsuppd  43639  radcnvrat  43751  nznngen  43753  trsspwALT3  44259  sspwimpALT2  44367  refsumcn  44392  iinssf  44504  icoiccdif  44909  icccncfext  45275  stoweidlem27  45415  stoweidlem46  45434  stoweidlem57  45445  fourierdlem40  45535  fourierdlem78  45572  ffnafv  46551  iccpartrn  46770  sprsymrelfvlem  46830  sprsymrelf1lem  46831  rhmsubcALTVlem4  47346  funcringcsetcALTV2lem8  47359  funcringcsetclem8ALTV  47382  ssnn0ssfz  47413  lincolss  47502  lcoss  47504  lcosslsp  47506  iunord  48107