Theorem ssrdv 3969

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  eqelssd  3985  ss2abdv  4046  sscon  4123  ssdif  4124  unss1  4165  ssrin  4222  eq0rdvALT  4388  sspw  4591  elpwdifsn  4770  uniss  4896  intss1  4944  intmin  4949  intssuni  4951  iinssiun  4986  iunss1  4987  iinss1  4988  ss2iun  4991  ssiun  5027  ssiun2  5028  iinss  5037  iinss2  5038  iunxdif3  5076  sspwb  5429  pwssun  5550  relop  5835  dmss  5887  dmcosseq  5961  dmcosseqOLD  5962  imadifssran  6145  ssrnres  6172  sossfld  6180  predtrss  6316  preddowncl  6326  tron  6380  tz7.7  6383  funimassd  6950  dffv2  6979  chfnrn  7044  fvn0ssdmfun  7069  fveqdmss  7073  dff3  7095  ffnfv  7114  f1imass  7262  ssorduni  7778  onint  7789  limsssuc  7850  limuni3  7852  limomss  7871  fo1stres  8019  fo2ndres  8020  fo2ndf  8125  fnse  8137  ressuppssdif  8189  suppss  8198  reldmtpos  8238  fprlem2  8305  onfununi  8360  smoiun  8380  smocdmdom  8387  tz7.48-1  8462  tz7.49  8464  oaass  8578  cofon1  8689  cofon2  8690  qsss  8797  uniinqs  8816  pmss12g  8888  mapss  8908  ixpssmap2g  8946  ixpssmapg  8947  pssnn  9187  fineqv  9276  finnzfsuppd  9390  ssfii  9436  dffi2  9440  oismo  9559  unxpwdom2  9607  inf3lemd  9646  inf3lem1  9647  inf3lem6  9652  cantnflem3  9710  cantnf  9712  cnfcom3lem  9722  onssr1  9850  rankunb  9869  tcrank  9903  harcard  9997  carduni  10000  infxpenlem  10032  infpwfien  10081  dfac12r  10166  ackbij2lem1  10237  ackbij1lem18  10255  isfin1-3  10405  fin1a2lem11  10429  fin1a2lem13  10431  zorn2lem4  10518  zorn2lem5  10519  ttukeylem6  10533  ttukeylem7  10534  fpwwe2lem10  10659  fpwwe2lem11  10660  fpwwe2  10662  wunr1om  10738  wunom  10739  tskr1om  10786  tskr1om2  10787  tskxpss  10791  tskcard  10800  tskuni  10802  grothomex  10848  genpss  11023  distrlem1pr  11044  distrlem5pr  11046  ltexprlem2  11056  ltexprlem6  11060  ltexprlem7  11061  reclem3pr  11068  reclem4pr  11069  supaddc  12214  supadd  12215  supmul1  12216  supmullem2  12218  peano5uzi  12687  uzss  12880  ixxdisj  13382  ixxss1  13385  ixxss2  13386  ixxss12  13387  ixxub  13388  ixxlb  13389  iocssre  13449  icossre  13450  iccssre  13451  icodisj  13498  fzss1  13585  fzss2  13586  ssfzunsnext  13591  fzosplit  13714  fzouzsplit  13716  ssfzo12bi  13782  ssnn0fi  14008  fsuppmapnn0fiub  14014  suppssfz  14017  sswrd  14545  rtrclreclem3  15084  isercoll  15689  summolem2a  15736  fsumcvg3  15750  fsum2dlem  15791  fsumcom2  15795  qshash  15848  prodmolem2a  15955  fprod2dlem  16001  fprodcom2  16005  bitsfzo  16459  1arith  16952  vdwlem2  17007  vdwlem6  17011  vdwlem8  17013  ramtlecl  17025  prmgaplem3  17078  prmgaplem4  17079  monhom  17753  epihom  17760  funcsetcres2  18111  funcestrcsetclem8  18164  funcsetcestrclem8  18179  psdmrn  18588  gsumwspan  18829  frmdss2  18846  sursubmefmnd  18879  injsubmefmnd  18880  trivsubgsnd  19142  ssnmz  19154  trivnsgd  19160  kerf1ghm  19235  conjnmz  19240  symgvalstruct  19383  gex1  19577  sylow2alem1  19603  lsmless1x  19630  lsmless2x  19631  lsmub1x  19632  lsmub2x  19633  lsmmod  19661  lsmdisj2  19668  efgrelexlemb  19736  efgcpbllemb  19741  cntzcmn  19826  gsum2d2  19960  dprdub  20013  dprdss  20017  dprddisj2  20027  pgpfac1lem3  20065  subrngmre  20527  subrguss  20552  subrgmre  20562  rnghmsscmap2  20594  rnghmsscmap  20595  funcrngcsetc  20605  funcrngcsetcALT  20606  rhmsscmap2  20623  rhmsscmap  20624  rhmsscrnghm  20630  rngcresringcat  20634  funcringcsetc  20639  unitrrg  20668  isdrng2  20708  primefld0cl  20771  primefld1cl  20772  lssssr  20916  lsssssubg  20920  lssmre  20928  lbspss  21045  lspdisj  21091  lbsextlem2  21125  lidl1el  21192  drngnidl  21209  lpiss  21295  zsssubrg  21398  qsssubdrg  21399  cnsubrg  21400  mulgrhm2  21444  znrrg  21531  ocvocv  21636  ocv2ss  21638  ocvin  21639  lsmcss  21657  cssmre  21658  pjcss  21681  lindfrn  21786  sraassab  21833  mhpsubg  22096  evls1maprnss  22321  dmatsgrp  22442  scmatsgrp  22462  scmatsgrp1  22465  m2cpmrngiso  22701  bastg  22909  tgss  22911  tgtop  22916  tgidm  22923  en2top  22928  neisspw  23050  topssnei  23067  neiptopuni  23073  lpss3  23087  clslp  23091  tgrest  23102  ssrest  23119  restntr  23125  ordtbas2  23134  ordtbas  23135  cnss1  23219  cnss2  23220  cnsscnp  23222  cnrest2r  23230  cmpsublem  23342  cmpsub  23343  tgcmp  23344  cmpcld  23345  hauscmplem  23349  cnconn  23365  llyss  23422  nllyss  23423  restnlly  23425  restlly  23426  locfincmp  23469  locfincf  23474  kgenss  23486  kgenidm  23490  llycmpkgen2  23493  1stckgen  23497  kgen2ss  23498  kgencn3  23501  ptbasfi  23524  ptpjopn  23555  txdis  23575  txkgen  23595  xkoptsub  23597  xkopjcn  23599  txconn  23632  qtoptop2  23642  qtopuni  23645  qtopkgen  23653  basqtop  23654  tgqtop  23655  qtopss  23658  qtoprest  23660  qtopomap  23661  qtopcmap  23662  kqsat  23674  kqcldsat  23676  hmphdis  23739  isfild  23801  ssfg  23815  fgss  23816  fgss2  23817  fgfil  23818  fgabs  23822  filconn  23826  fgtr  23833  uzrest  23840  ufilmax  23850  ufileu  23862  filufint  23863  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  flimss2  23915  flimss1  23916  flimclsi  23921  flimcf  23925  flimsncls  23929  fclssscls  23961  fclsss1  23965  fclsss2  23966  fclscf  23968  uffclsflim  23974  alexsublem  23987  alexsubALTlem3  23992  ptcmplem2  23996  ptcmplem3  23997  cnextf  24009  efmndtmd  24044  symgtgp  24049  cldsubg  24054  tsmscl  24078  haustsms2  24080  tgptsmscls  24093  tsmsxp  24098  restutop  24181  ustuqtop4  24188  utop2nei  24194  utop3cls  24195  ucncn  24228  xblss2ps  24345  xblss2  24346  xrsblre  24756  xrsmopn  24757  recld2  24759  zdis  24761  icccmplem2  24768  cncfss  24848  cnheiborlem  24909  htpycn  24928  phtpyhtpy  24937  pi1blem  24995  cphsscph  25208  cfilfcls  25231  iscmet3lem2  25249  iscmet2  25251  caussi  25254  equivcfil  25256  lmcau  25270  metsscmetcld  25272  hlhil  25400  ivthicc  25416  ovoliunnul  25465  ovolicopnf  25482  uniioombllem3  25543  dyadmbllem  25557  volsup2  25563  vitalilem2  25567  itg1addlem4  25657  itg10a  25668  itg1ge0a  25669  mbfi1fseqlem4  25676  itg2gt0  25718  limciun  25852  perfdvf  25861  cpnord  25894  dvcj  25911  dvlip2  25957  dvivth  25972  dvne0  25973  dvcnvre  25981  ply1lpir  26144  plyco0  26154  plyexmo  26278  abelth  26408  efif1o  26512  logno1  26602  efopnlem2  26623  loglesqrt  26728  lgamcvg2  27022  ppisval  27071  ppinprm  27119  chtnprm  27121  fsumvma  27181  dchrfi  27223  chtppilimlem2  27442  chebbnd2  27445  vmadivsumb  27451  rplogsumlem2  27453  dchrisumlem2  27458  vmalogdivsum2  27506  vmalogdivsum  27507  2vmadivsumlem  27508  selbergb  27517  selberg2b  27520  selberg3lem1  27525  selberg3lem2  27526  selberg3  27527  selberg4lem1  27528  selberg4  27529  pntrlog2bndlem2  27546  pntrlog2bndlem4  27548  oldssmade  27846  sltlpss  27876  noseqrdgfn  28257  peano5uzs  28349  uhgredgss  29115  usgruspgrb  29167  uhgrissubgr  29259  uhgrspansubgrlem  29274  uhgrspan1  29287  cusgredg  29408  usgredgsscusgredg  29444  ococss  31279  shsub1  31310  shless  31345  shmodsi  31375  pjhth  31379  spansnss  31557  spanpr  31566  spansnm0i  31636  pjjsi  31686  sumdmdii  32401  sumdmdlem  32404  sumdmdlem2  32405  cdj3lem1  32420  abrexss  32498  fnpreimac  32654  rnmposs  32657  unifi3  32695  uzssico  32766  ssnnssfz  32769  pwrssmgc  32985  pmtrcnel  33105  cycpmrn  33159  cyc3evpm  33166  cycpmgcl  33169  elrgspnlem1  33242  elrgspnlem3  33244  elrgspnlem4  33245  elrgspnsubrunlem2  33248  fldgensdrg  33313  ringlsmss1  33416  ringlsmss2  33417  prmidlssidl  33465  mxidlirredi  33491  drngmxidl  33497  drngmxidlr  33498  1arithidomlem1  33555  1arithidom  33557  1arithufdlem2  33565  1arithufdlem3  33566  1arithufdlem4  33567  dfufd2lem  33569  ply1mulrtss  33599  dimkerim  33672  extdg1id  33712  irngss  33733  irngssv  33734  algextdeglem8  33763  constrsscn  33779  constrsslem  33780  constrsdrg  33814  crefss  33885  cmpcref  33886  zarmxt1  33916  tpr2rico  33948  esumrnmpt2  34104  esumpcvgval  34114  ldsysgenld  34196  sigapildsys  34198  ldgenpisys  34202  cldssbrsiga  34223  measdivcstALTV  34261  mbfmcnt  34305  oddpwdc  34391  eulerpartlemgs2  34417  reprpmtf1o  34663  bnj1033  35005  bnj1398  35070  sconnpi1  35266  cvmscld  35300  cvmliftlem15  35325  satfrnmapom  35397  dfon2lem6  35811  fnessref  36380  fgmin  36393  tailfb  36400  dissneqlem  37363  icoreresf  37375  rdglimss  37400  finxpreclem6  37419  lindsenlbs  37644  poimirlem11  37660  poimirlem12  37661  sstotbnd3  37805  prdstotbnd  37823  cntotbnd  37825  ismtyhmeo  37834  1idl  38055  disjdmqsss  38825  lshpdisj  39010  lssats  39035  lkrin  39187  glbconxN  39402  paddss1  39841  paddss2  39842  paddasslem16  39859  paddidm  39865  pmodlem2  39871  pmapjoin  39876  pmapjat1  39877  pclfinN  39924  pclfinclN  39974  diasslssN  41083  dia2dimlem12  41099  dihsslss  41300  baerlem3lem2  41734  baerlem5alem2  41735  baerlem5blem2  41736  zndvdchrrhm  41990  dvrelog2  42082  dvrelog3  42083  aks4d1p3  42096  aks4d1p4  42097  aks4d1p5  42098  aks4d1p7  42101  aks4d1p8  42105  primrootsunit1  42115  primrootscoprmpow  42117  primrootscoprbij  42120  hashscontpow1  42139  aks6d1c4  42142  sticksstones3  42166  aks6d1c6lem3  42190  aks6d1c6isolem2  42193  aks6d1c6lem5  42195  rhmqusspan  42203  unitscyglem1  42213  unitscyglem4  42216  ss2ab1  42237  eldiophss  42772  rencldnfilem  42818  pellexlem5  42831  pell14qrss1234  42854  pell1qrss14  42866  pellfundre  42879  pellfundge  42880  pellfundlb  42882  pellfundglb  42883  harinf  43033  proot1hash  43194  safesnsupfiss  43414  intabssd  43518  ss2iundf  43658  ov2ssiunov2  43699  clsk1indlem3  44042  radcnvrat  44313  nznngen  44315  trsspwALT3  44819  sspwimpALT2  44927  refsumcn  45034  iinssf  45142  icoiccdif  45533  icccncfext  45896  stoweidlem27  46036  stoweidlem46  46055  stoweidlem57  46066  fourierdlem40  46156  fourierdlem78  46193  ffnafv  47180  iccpartrn  47424  sprsymrelfvlem  47484  sprsymrelf1lem  47485  clnbgrssedg  47834  stgrusgra  47951  rhmsubcALTVlem4  48239  funcringcsetcALTV2lem8  48252  funcringcsetclem8ALTV  48275  ssnn0ssfz  48304  lincolss  48390  lcoss  48392  lcosslsp  48394  iunord  49520