Theorem ssrdv 3941

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  eqelssd  3957  ss2abim  4014  ss2abdv  4019  sscon  4097  ssdif  4098  unss1  4139  ssrin  4196  eq0rdvALT  4362  sspw  4567  elpwdifsn  4747  uniss  4873  intss1  4920  intmin  4925  intssuni  4927  iinssiun  4962  iunss1  4963  iinss1  4964  ss2iun  4967  ssiun  5004  ssiun2  5005  iinss  5014  iinss2  5015  iunxdif3  5052  sspwb  5404  pwssun  5524  relop  5807  dmss  5859  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  imadifssran  6117  ssrnres  6144  sossfld  6152  predtrss  6288  preddowncl  6298  tron  6348  tz7.7  6351  funimassd  6908  dffv2  6937  chfnrn  7003  fvn0ssdmfun  7028  fveqdmss  7032  dff3  7054  ffnfv  7073  f1imass  7220  ssorduni  7734  onint  7745  limsssuc  7802  limuni3  7804  limomss  7823  fo1stres  7969  fo2ndres  7970  fo2ndf  8073  fnse  8085  ressuppssdif  8137  suppss  8146  reldmtpos  8186  fprlem2  8253  onfununi  8283  smoiun  8303  smocdmdom  8310  tz7.48-1  8384  tz7.49  8386  oaass  8498  cofon1  8610  cofon2  8611  qsss  8724  uniinqs  8746  pmss12g  8819  mapss  8839  ixpssmap2g  8877  ixpssmapg  8878  pssnn  9105  fineqv  9179  unifi3  9274  finnzfsuppd  9288  ssfii  9334  dffi2  9338  oismo  9457  unxpwdom2  9505  inf3lemd  9548  inf3lem1  9549  inf3lem6  9554  cantnflem3  9612  cantnf  9614  cnfcom3lem  9624  onssr1  9755  rankunb  9774  tcrank  9808  harcard  9902  carduni  9905  infxpenlem  9935  infpwfien  9984  dfac12r  10069  ackbij2lem1  10140  ackbij1lem18  10158  isfin1-3  10308  fin1a2lem11  10332  fin1a2lem13  10334  zorn2lem4  10421  zorn2lem5  10422  ttukeylem6  10436  ttukeylem7  10437  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2  10566  wunr1om  10642  wunom  10643  tskr1om  10690  tskr1om2  10691  tskxpss  10695  tskcard  10704  tskuni  10706  grothomex  10752  genpss  10927  distrlem1pr  10948  distrlem5pr  10950  ltexprlem2  10960  ltexprlem6  10964  ltexprlem7  10965  reclem3pr  10972  reclem4pr  10973  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  peano5uzi  12593  uzss  12786  ixxdisj  13288  ixxss1  13291  ixxss2  13292  ixxss12  13293  ixxub  13294  ixxlb  13295  iocssre  13355  icossre  13356  iccssre  13357  icodisj  13404  fzss1  13491  fzss2  13492  ssfzunsnext  13497  fzosplit  13620  fzouzsplit  13622  ssfzo12bi  13689  ssnn0fi  13920  fsuppmapnn0fiub  13926  suppssfz  13929  sswrd  14457  rtrclreclem3  14995  isercoll  15603  summolem2a  15650  fsumcvg3  15664  fsum2dlem  15705  fsumcom2  15709  qshash  15762  prodmolem2a  15869  fprod2dlem  15915  fprodcom2  15919  bitsfzo  16374  1arith  16867  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  ramtlecl  16940  prmgaplem3  16993  prmgaplem4  16994  monhom  17671  epihom  17678  funcsetcres2  18029  funcestrcsetclem8  18082  funcsetcestrclem8  18097  psdmrn  18508  chnrss  18550  chndss  18551  gsumwspan  18783  frmdss2  18800  sursubmefmnd  18833  injsubmefmnd  18834  trivsubgsnd  19095  ssnmz  19107  trivnsgd  19113  kerf1ghm  19188  conjnmz  19193  symgvalstruct  19338  gex1  19532  sylow2alem1  19558  lsmless1x  19585  lsmless2x  19586  lsmub1x  19587  lsmub2x  19588  lsmmod  19616  lsmdisj2  19623  efgrelexlemb  19691  efgcpbllemb  19696  cntzcmn  19781  gsum2d2  19915  dprdub  19968  dprdss  19972  dprddisj2  19982  pgpfac1lem3  20020  subrngmre  20507  subrguss  20532  subrgmre  20542  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  rngcresringcat  20614  funcringcsetc  20619  unitrrg  20648  isdrng2  20688  primefld0cl  20751  primefld1cl  20752  lssssr  20917  lsssssubg  20921  lssmre  20929  lbspss  21046  lspdisj  21092  lbsextlem2  21126  lidl1el  21193  drngnidl  21210  lpiss  21296  zsssubrg  21392  qsssubdrg  21393  cnsubrg  21394  mulgrhm2  21445  znrrg  21532  ocvocv  21638  ocv2ss  21640  ocvin  21641  lsmcss  21659  cssmre  21660  pjcss  21683  lindfrn  21788  sraassab  21835  mhpsubg  22108  evls1maprnss  22334  dmatsgrp  22455  scmatsgrp  22475  scmatsgrp1  22478  m2cpmrngiso  22714  bastg  22922  tgss  22924  tgtop  22929  tgidm  22936  en2top  22941  neisspw  23063  topssnei  23080  neiptopuni  23086  lpss3  23100  clslp  23104  tgrest  23115  ssrest  23132  restntr  23138  ordtbas2  23147  ordtbas  23148  cnss1  23232  cnss2  23233  cnsscnp  23235  cnrest2r  23243  cmpsublem  23355  cmpsub  23356  tgcmp  23357  cmpcld  23358  hauscmplem  23362  cnconn  23378  llyss  23435  nllyss  23436  restnlly  23438  restlly  23439  locfincmp  23482  locfincf  23487  kgenss  23499  kgenidm  23503  llycmpkgen2  23506  1stckgen  23510  kgen2ss  23511  kgencn3  23514  ptbasfi  23537  ptpjopn  23568  txdis  23588  txkgen  23608  xkoptsub  23610  xkopjcn  23612  txconn  23645  qtoptop2  23655  qtopuni  23658  qtopkgen  23666  basqtop  23667  tgqtop  23668  qtopss  23671  qtoprest  23673  qtopomap  23674  qtopcmap  23675  kqsat  23687  kqcldsat  23689  hmphdis  23752  isfild  23814  ssfg  23828  fgss  23829  fgss2  23830  fgfil  23831  fgabs  23835  filconn  23839  fgtr  23846  uzrest  23853  ufilmax  23863  ufileu  23875  filufint  23876  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  flimss2  23928  flimss1  23929  flimclsi  23934  flimcf  23938  flimsncls  23942  fclssscls  23974  fclsss1  23978  fclsss2  23979  fclscf  23981  uffclsflim  23987  alexsublem  24000  alexsubALTlem3  24005  ptcmplem2  24009  ptcmplem3  24010  cnextf  24022  efmndtmd  24057  symgtgp  24062  cldsubg  24067  tsmscl  24091  haustsms2  24093  tgptsmscls  24106  tsmsxp  24111  restutop  24193  ustuqtop4  24200  utop2nei  24206  utop3cls  24207  ucncn  24240  xblss2ps  24357  xblss2  24358  xrsblre  24768  xrsmopn  24769  recld2  24771  zdis  24773  icccmplem2  24780  cncfss  24860  cnheiborlem  24921  htpycn  24940  phtpyhtpy  24949  pi1blem  25007  cphsscph  25219  cfilfcls  25242  iscmet3lem2  25260  iscmet2  25262  caussi  25265  equivcfil  25267  lmcau  25281  metsscmetcld  25283  hlhil  25411  ivthicc  25427  ovoliunnul  25476  ovolicopnf  25493  uniioombllem3  25554  dyadmbllem  25568  volsup2  25574  vitalilem2  25578  itg1addlem4  25668  itg10a  25679  itg1ge0a  25680  mbfi1fseqlem4  25687  itg2gt0  25729  limciun  25863  perfdvf  25872  cpnord  25905  dvcj  25922  dvlip2  25968  dvivth  25983  dvne0  25984  dvcnvre  25992  ply1lpir  26155  plyco0  26165  plyexmo  26289  abelth  26419  efif1o  26523  logno1  26613  efopnlem2  26634  loglesqrt  26739  lgamcvg2  27033  ppisval  27082  ppinprm  27130  chtnprm  27132  fsumvma  27192  dchrfi  27234  chtppilimlem2  27453  chebbnd2  27456  vmadivsumb  27462  rplogsumlem2  27464  dchrisumlem2  27469  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  selbergb  27528  selberg2b  27531  selberg3lem1  27536  selberg3lem2  27537  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  oldssmade  27875  ltslpss  27916  noseqrdgfn  28314  n0ssoldg  28361  peano5uzs  28412  uhgredgss  29216  usgruspgrb  29268  uhgrissubgr  29360  uhgrspansubgrlem  29375  uhgrspan1  29388  cusgredg  29509  usgredgsscusgredg  29545  ococss  31381  shsub1  31412  shless  31447  shmodsi  31477  pjhth  31481  spansnss  31659  spanpr  31668  spansnm0i  31738  pjjsi  31788  sumdmdii  32503  sumdmdlem  32506  sumdmdlem2  32507  cdj3lem1  32522  abrexss  32599  fnpreimac  32760  rnmposs  32763  uzssico  32875  ssnnssfz  32878  pwrssmgc  33093  pmtrcnel  33183  cycpmrn  33237  cyc3evpm  33244  cycpmgcl  33247  elrgspnlem1  33336  elrgspnlem3  33338  elrgspnlem4  33339  elrgspnsubrunlem2  33342  fldgensdrg  33408  ringlsmss1  33489  ringlsmss2  33490  prmidlssidl  33538  mxidlirredi  33564  drngmxidl  33570  drngmxidlr  33571  1arithidomlem1  33628  1arithidom  33630  1arithufdlem2  33638  1arithufdlem3  33639  1arithufdlem4  33640  dfufd2lem  33642  ply1mulrtss  33675  esplyfvaln  33751  dimkerim  33805  extdg1id  33844  irngss  33865  irngssv  33866  algextdeglem8  33902  constrsscn  33918  constrsslem  33919  constrsdrg  33953  crefss  34027  cmpcref  34028  zarmxt1  34058  tpr2rico  34090  esumrnmpt2  34246  esumpcvgval  34256  ldsysgenld  34338  sigapildsys  34340  ldgenpisys  34344  cldssbrsiga  34365  measdivcstALTV  34403  mbfmcnt  34446  oddpwdc  34532  eulerpartlemgs2  34558  reprpmtf1o  34804  bnj1033  35145  bnj1398  35210  trssfir1om  35289  r1omhfb  35290  trssfir1omregs  35314  r1omhfbregs  35315  sconnpi1  35455  cvmscld  35489  cvmliftlem15  35514  satfrnmapom  35586  dfon2lem6  36002  fnessref  36573  fgmin  36586  tailfb  36593  dissneqlem  37595  icoreresf  37607  rdglimss  37632  finxpreclem6  37651  lindsenlbs  37866  poimirlem11  37882  poimirlem12  37883  sstotbnd3  38027  prdstotbnd  38045  cntotbnd  38047  ismtyhmeo  38056  1idl  38277  disjdmqsss  39156  lshpdisj  39363  lssats  39388  lkrin  39540  glbconxN  39754  paddss1  40193  paddss2  40194  paddasslem16  40211  paddidm  40217  pmodlem2  40223  pmapjoin  40228  pmapjat1  40229  pclfinN  40276  pclfinclN  40326  diasslssN  41435  dia2dimlem12  41451  dihsslss  41652  baerlem3lem2  42086  baerlem5alem2  42087  baerlem5blem2  42088  zndvdchrrhm  42342  dvrelog2  42434  dvrelog3  42435  aks4d1p3  42448  aks4d1p4  42449  aks4d1p5  42450  aks4d1p7  42453  aks4d1p8  42457  primrootsunit1  42467  primrootscoprmpow  42469  primrootscoprbij  42472  hashscontpow1  42491  aks6d1c4  42494  sticksstones3  42518  aks6d1c6lem3  42542  aks6d1c6isolem2  42545  aks6d1c6lem5  42547  rhmqusspan  42555  unitscyglem1  42565  unitscyglem4  42568  eldiophss  43131  rencldnfilem  43177  pellexlem5  43190  pell14qrss1234  43213  pell1qrss14  43225  pellfundre  43238  pellfundge  43239  pellfundlb  43241  pellfundglb  43242  harinf  43391  proot1hash  43552  safesnsupfiss  43771  intabssd  43875  ss2iundf  44015  ov2ssiunov2  44056  clsk1indlem3  44399  radcnvrat  44670  nznngen  44672  trsspwALT3  45175  sspwimpALT2  45283  refsumcn  45390  iinssf  45497  icoiccdif  45884  icccncfext  46245  stoweidlem27  46385  stoweidlem46  46404  stoweidlem57  46415  fourierdlem40  46505  fourierdlem78  46542  ffnafv  47531  iccpartrn  47790  sprsymrelfvlem  47850  sprsymrelf1lem  47851  clnbgrssedg  48201  stgrusgra  48319  rhmsubcALTVlem4  48644  funcringcsetcALTV2lem8  48657  funcringcsetclem8ALTV  48680  ssnn0ssfz  48709  lincolss  48794  lcoss  48796  lcosslsp  48798  iunord  50035