Theorem ssrdv 3951

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

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ss 3930

This theorem is referenced by:  eqelssd  3966  ss2abim  4022  ss2abdv  4027  sscon  4105  ssdif  4106  unss1  4146  ssrin  4202  eq0rdvALT  4371  sspw  4575  elpwdifsn  4758  uniss  4881  intss1  4929  intmin  4934  intssuni  4936  iinssiun  4971  iunss1  4972  iinss1  4973  ss2iun  4976  ssiun  5012  ssiun2  5013  iinss  5022  iinss2  5023  iunxdif3  5062  sspwb  5428  pwssun  5551  relop  5834  dmss  5890  dmcosseq  5966  dmcosseqOLD  5967  ssrnres  6174  sossfld  6182  imadifssran  6200  imadifssranOLD  6201  predtrss  6321  preddowncl  6331  tron  6381  tz7.7  6384  funimassd  6945  dffv2  6974  chfnrn  7042  fvn0ssdmfun  7067  fveqdmss  7071  dff3  7093  ffnfv  7112  f1imass  7260  ssorduni  7774  onint  7785  limsssuc  7842  limuni3  7844  limomss  7863  fo1stres  8008  fo2ndres  8009  fo2ndf  8112  fnse  8125  ressuppssdif  8177  suppss  8186  reldmtpos  8226  fprlem2  8294  onfununi  8324  smoiun  8344  smocdmdom  8351  tz7.48-1  8426  tz7.49  8428  oaass  8542  cofon1  8654  cofon2  8655  qsss  8769  uniinqs  8791  pmss12g  8863  mapss  8883  ixpssmap2g  8921  ixpssmapg  8922  pssnn  9149  fineqv  9223  unifi3  9315  finnzfsuppd  9329  ssfii  9375  dffi2  9379  oismo  9498  unxpwdom2  9546  inf3lemd  9592  inf3lem1  9593  inf3lem6  9598  cantnflem3  9656  cantnf  9658  cnfcom3lem  9668  onssr1  9799  rankunb  9818  tcrank  9852  harcard  9960  carduni  9963  infxpenlem  9993  infpwfien  10042  dfac12r  10126  ackbij2lem1  10197  ackbij1lem18  10215  isfin1-3  10366  fin1a2lem11  10390  fin1a2lem13  10392  zorn2lem4  10479  zorn2lem5  10480  ttukeylem6  10494  ttukeylem7  10495  fpwwe2lem10  10621  fpwwe2lem11  10622  fpwwe2  10624  wunr1om  10700  wunom  10701  tskr1om  10748  tskr1om2  10749  tskxpss  10753  tskcard  10762  tskuni  10764  grothomex  10810  genpss  10985  distrlem1pr  11006  distrlem5pr  11008  ltexprlem2  11018  ltexprlem6  11022  ltexprlem7  11023  reclem3pr  11030  reclem4pr  11031  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  peano5uzi  12681  uzss  12881  ixxdisj  13383  ixxss1  13386  ixxss2  13387  ixxss12  13388  ixxub  13389  ixxlb  13390  iocssre  13450  icossre  13451  iccssre  13452  icodisj  13499  fzss1  13587  fzss2  13588  ssfzunsnext  13593  fzosplit  13717  fzouzsplit  13719  ssfzo12bi  13786  ssnn0fi  14017  fsuppmapnn0fiub  14023  suppssfz  14026  sswrd  14555  rtrclreclem3  15093  isercoll  15715  summolem2a  15762  fsumcvg3  15776  fsum2dlem  15817  fsumcom2  15821  qshash  15875  prodmolem2a  15984  fprod2dlem  16030  fprodcom2  16034  bitsfzo  16489  1arith  16983  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  ramtlecl  17056  prmgaplem3  17109  prmgaplem4  17110  monhom  17788  epihom  17795  funcsetcres2  18146  funcestrcsetclem8  18199  funcsetcestrclem8  18214  psdmrn  18625  chnrss  18667  chndss  18668  gsumwspan  18901  frmdss2  18918  sursubmefmnd  18951  injsubmefmnd  18952  trivsubgsnd  19216  ssnmz  19228  trivnsgd  19234  kerf1ghm  19313  conjnmz  19318  symgvalstruct  19463  gex1  19657  sylow2alem1  19683  lsmless1x  19710  lsmless2x  19711  lsmub1x  19712  lsmub2x  19713  lsmmod  19741  lsmdisj2  19748  efgrelexlemb  19816  efgcpbllemb  19821  cntzcmn  19906  gsum2d2  20040  dprdub  20093  dprdss  20097  dprddisj2  20107  pgpfac1lem3  20145  subrngmre  20643  subrguss  20668  subrgmre  20678  rnghmsscmap2  20710  rnghmsscmap  20711  funcrngcsetc  20721  funcrngcsetcALT  20722  rhmsscmap2  20739  rhmsscmap  20740  rhmsscrnghm  20746  rngcresringcat  20750  funcringcsetc  20755  unitrrg  20784  isdrng2  20823  primefld0cl  20883  primefld1cl  20884  lssssr  21049  lsssssubg  21053  lssmre  21061  lbspss  21177  lspdisj  21223  lbsextlem2  21257  lidl1el  21325  drngnidl  21347  prmidlssidl  21437  lpiss  21462  zsssubrg  21540  qsssubdrg  21541  cnsubrg  21542  mulgrhm2  21593  znrrg  21680  ocvocv  21786  ocv2ss  21788  ocvin  21789  lsmcss  21807  cssmre  21808  pjcss  21831  lindfrn  21936  sraassab  21983  mhpsubg  22281  evls1maprnss  22503  dmatsgrp  22621  scmatsgrp  22641  scmatsgrp1  22644  m2cpmrngiso  22880  bastg  23088  tgss  23090  tgtop  23095  tgidm  23102  en2top  23107  neisspw  23229  topssnei  23246  neiptopuni  23252  lpss3  23266  clslp  23270  tgrest  23281  ssrest  23298  restntr  23304  ordtbas2  23313  ordtbas  23314  cnss1  23398  cnss2  23399  cnsscnp  23401  cnrest2r  23409  cmpsublem  23521  cmpsub  23522  tgcmp  23523  cmpcld  23524  hauscmplem  23528  cnconn  23544  llyss  23601  nllyss  23602  restnlly  23604  restlly  23605  locfincmp  23648  locfincf  23653  kgenss  23665  kgenidm  23669  llycmpkgen2  23672  1stckgen  23676  kgen2ss  23677  kgencn3  23680  ptbasfi  23703  ptpjopn  23734  txdis  23754  txkgen  23774  xkoptsub  23776  xkopjcn  23778  txconn  23811  qtoptop2  23821  qtopuni  23824  qtopkgen  23832  basqtop  23833  tgqtop  23834  qtopss  23837  qtoprest  23839  qtopomap  23840  qtopcmap  23841  kqsat  23853  kqcldsat  23855  hmphdis  23918  isfild  23980  ssfg  23994  fgss  23995  fgss2  23996  fgfil  23997  fgabs  24001  filconn  24005  fgtr  24012  uzrest  24019  ufilmax  24029  ufileu  24041  filufint  24042  rnelfm  24075  fmfnfmlem2  24077  fmfnfmlem4  24079  flimss2  24094  flimss1  24095  flimclsi  24100  flimcf  24104  flimsncls  24108  fclssscls  24140  fclsss1  24144  fclsss2  24145  fclscf  24147  uffclsflim  24153  alexsublem  24166  alexsubALTlem3  24171  ptcmplem2  24175  ptcmplem3  24176  cnextf  24188  efmndtmd  24223  symgtgp  24228  cldsubg  24233  tsmscl  24257  haustsms2  24259  tgptsmscls  24272  tsmsxp  24277  restutop  24359  ustuqtop4  24366  utop2nei  24372  utop3cls  24373  ucncn  24406  xblss2ps  24523  xblss2  24524  xrsblre  24934  xrsmopn  24935  recld2  24937  zdis  24939  icccmplem2  24946  cncfss  25023  cnheiborlem  25078  htpycn  25097  phtpyhtpy  25106  pi1blem  25163  cphsscph  25375  cfilfcls  25398  iscmet3lem2  25416  iscmet2  25418  caussi  25421  equivcfil  25423  lmcau  25437  metsscmetcld  25439  hlhil  25567  ivthicc  25582  ovoliunnul  25631  ovolicopnf  25648  uniioombllem3  25709  dyadmbllem  25723  volsup2  25729  vitalilem2  25733  itg1addlem4  25823  itg10a  25834  itg1ge0a  25835  mbfi1fseqlem4  25842  itg2gt0  25884  limciun  26018  perfdvf  26027  cpnord  26059  dvcj  26074  dvlip2  26119  dvivth  26134  dvne0  26135  dvcnvre  26143  ply1lpir  26304  plyco0  26314  plyexmo  26439  abelth  26566  efif1o  26673  logno1  26763  efopnlem2  26784  loglesqrt  26888  lgamcvg2  27181  ppisval  27230  ppinprm  27278  chtnprm  27280  fsumvma  27339  dchrfi  27381  chtppilimlem2  27600  chebbnd2  27603  vmadivsumb  27609  rplogsumlem2  27611  dchrisumlem2  27616  vmalogdivsum2  27664  vmalogdivsum  27665  2vmadivsumlem  27666  selbergb  27675  selberg2b  27678  selberg3lem1  27683  selberg3lem2  27684  selberg3  27685  selberg4lem1  27686  selberg4  27687  pntrlog2bndlem2  27704  pntrlog2bndlem4  27706  oldssmade  28022  ltslpss  28063  noseqrdgfn  28461  n0ssoldg  28508  peano5uzs  28559  elplnglnid  29019  lnincplng  29020  plngrotlem2  29024  prlngpln3  29148  uhgredgss  29418  usgruspgrb  29470  uhgrissubgr  29562  uhgrspansubgrlem  29577  uhgrspan1  29590  cusgredg  29711  usgredgsscusgredg  29746  ococss  31582  shsub1  31613  shless  31648  shmodsi  31678  pjhth  31682  spansnss  31860  spanpr  31869  spansnm0i  31939  pjjsi  31989  sumdmdii  32704  sumdmdlem  32707  sumdmdlem2  32708  cdj3lem1  32723  abrexss  32795  fnpreimac  32952  rnmposs  32955  uzssico  33066  ssnnssfz  33069  pwrssmgc  33257  pmtrcnel  33346  cycpmrn  33400  cyc3evpm  33407  cycpmgcl  33410  elrgspnlem1  33499  elrgspnlem3  33501  elrgspnlem4  33502  elrgspnsubrunlem2  33505  fldgensdrg  33574  ringlsmss1  33647  ringlsmss2  33648  mxidlirredi  33695  drngmxidl  33700  drngmxidlr  33701  1arithidomlem1  33766  1arithidom  33768  1arithufdlem2  33776  1arithufdlem3  33777  1arithufdlem4  33778  dfufd2lem  33780  ply1mulrtss  33813  esplyfvaln  33905  dimkerim  33958  extdg1id  33997  irngss  34018  irngssv  34019  algextdeglem8  34055  constrsscn  34071  constrsslem  34072  constrsdrg  34106  crefss  34180  cmpcref  34181  zarmxt1  34211  tpr2rico  34243  esumrnmpt2  34399  esumpcvgval  34409  ldsysgenld  34491  sigapildsys  34493  ldgenpisys  34497  cldssbrsiga  34518  measdivcstALTV  34556  mbfmcnt  34599  oddpwdc  34685  eulerpartlemgs2  34711  reprpmtf1o  34954  bnj1033  35298  bnj1398  35363  trssfir1om  35443  r1omhfb  35444  trssfir1omregs  35468  r1omhfbregs  35469  sconnpi1  35626  cvmscld  35660  cvmliftlem15  35685  satfrnmapom  35757  dfon2lem6  36173  fnessref  36753  fgmin  36766  tailfb  36773  dissneqlem  37869  icoreresf  37881  rdglimss  37906  finxpreclem6  37925  lindsenlbs  38149  poimirlem11  38165  poimirlem12  38166  sstotbnd3  38310  prdstotbnd  38328  cntotbnd  38330  ismtyhmeo  38339  1idl  38560  disjdmqsss  39439  lshpdisj  39646  lssats  39671  lkrin  39823  glbconxN  40037  paddss1  40476  paddss2  40477  paddasslem16  40494  paddidm  40500  pmodlem2  40506  pmapjoin  40511  pmapjat1  40512  pclfinN  40559  pclfinclN  40609  diasslssN  41718  dia2dimlem12  41734  dihsslss  41935  baerlem3lem2  42369  baerlem5alem2  42370  baerlem5blem2  42371  zndvdchrrhm  42625  dvrelog2  42716  dvrelog3  42717  aks4d1p3  42730  aks4d1p4  42731  aks4d1p5  42732  aks4d1p7  42735  aks4d1p8  42739  primrootsunit1  42749  primrootscoprmpow  42751  primrootscoprbij  42754  hashscontpow1  42773  aks6d1c4  42776  sticksstones3  42800  aks6d1c6lem3  42824  aks6d1c6isolem2  42827  aks6d1c6lem5  42829  rhmqusspan  42837  unitscyglem1  42847  unitscyglem4  42850  eldiophss  43392  rencldnfilem  43434  pellexlem5  43447  pell14qrss1234  43470  pell1qrss14  43482  pellfundre  43495  pellfundge  43496  pellfundlb  43498  pellfundglb  43499  harinf  43648  proot1hash  43809  safesnsupfiss  44028  intabssd  44132  ss2iundf  44272  ov2ssiunov2  44313  clsk1indlem3  44656  radcnvrat  44911  nznngen  44913  trsspwALT3  45415  sspwimpALT2  45523  refsumcn  45637  iinssf  45743  icoiccdif  46127  icccncfext  46488  stoweidlem27  46628  stoweidlem46  46647  stoweidlem57  46658  fourierdlem40  46748  fourierdlem78  46785  ffnafv  47792  iccpartrn  48063  sprsymrelfvlem  48123  sprsymrelf1lem  48124  clnbgrssedg  48490  stgrusgra  48608  rhmsubcALTVlem4  48933  funcringcsetcALTV2lem8  48946  funcringcsetclem8ALTV  48969  ssnn0ssfz  49009  lincolss  49094  lcoss  49096  lcosslsp  49098  iunord  50334