Theorem ssrdv 3927

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

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

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 3906

This theorem is referenced by:  eqelssd  3943  ss2abim  4000  ss2abdv  4005  sscon  4083  ssdif  4084  unss1  4125  ssrin  4182  eq0rdvALT  4348  sspw  4552  elpwdifsn  4734  uniss  4858  intss1  4905  intmin  4910  intssuni  4912  iinssiun  4947  iunss1  4948  iinss1  4949  ss2iun  4952  ssiun  4989  ssiun2  4990  iinss  4999  iinss2  5000  iunxdif3  5037  sspwb  5401  pwssun  5523  relop  5805  dmss  5857  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  imadifssran  6115  ssrnres  6142  sossfld  6150  predtrss  6286  preddowncl  6296  tron  6346  tz7.7  6349  funimassd  6906  dffv2  6935  chfnrn  7001  fvn0ssdmfun  7026  fveqdmss  7030  dff3  7052  ffnfv  7071  f1imass  7219  ssorduni  7733  onint  7744  limsssuc  7801  limuni3  7803  limomss  7822  fo1stres  7968  fo2ndres  7969  fo2ndf  8071  fnse  8083  ressuppssdif  8135  suppss  8144  reldmtpos  8184  fprlem2  8251  onfununi  8281  smoiun  8301  smocdmdom  8308  tz7.48-1  8382  tz7.49  8384  oaass  8496  cofon1  8608  cofon2  8609  qsss  8722  uniinqs  8744  pmss12g  8817  mapss  8837  ixpssmap2g  8875  ixpssmapg  8876  pssnn  9103  fineqv  9177  unifi3  9272  finnzfsuppd  9286  ssfii  9332  dffi2  9336  oismo  9455  unxpwdom2  9503  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  12123  supadd  12124  supmul1  12125  supmullem2  12127  peano5uzi  12618  uzss  12811  ixxdisj  13313  ixxss1  13316  ixxss2  13317  ixxss12  13318  ixxub  13319  ixxlb  13320  iocssre  13380  icossre  13381  iccssre  13382  icodisj  13429  fzss1  13517  fzss2  13518  ssfzunsnext  13523  fzosplit  13647  fzouzsplit  13649  ssfzo12bi  13716  ssnn0fi  13947  fsuppmapnn0fiub  13953  suppssfz  13956  sswrd  14484  rtrclreclem3  15022  isercoll  15630  summolem2a  15677  fsumcvg3  15691  fsum2dlem  15732  fsumcom2  15736  qshash  15790  prodmolem2a  15899  fprod2dlem  15945  fprodcom2  15949  bitsfzo  16404  1arith  16898  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  ramtlecl  16971  prmgaplem3  17024  prmgaplem4  17025  monhom  17702  epihom  17709  funcsetcres2  18060  funcestrcsetclem8  18113  funcsetcestrclem8  18128  psdmrn  18539  chnrss  18581  chndss  18582  gsumwspan  18814  frmdss2  18831  sursubmefmnd  18864  injsubmefmnd  18865  trivsubgsnd  19129  ssnmz  19141  trivnsgd  19147  kerf1ghm  19222  conjnmz  19227  symgvalstruct  19372  gex1  19566  sylow2alem1  19592  lsmless1x  19619  lsmless2x  19620  lsmub1x  19621  lsmub2x  19622  lsmmod  19650  lsmdisj2  19657  efgrelexlemb  19725  efgcpbllemb  19730  cntzcmn  19815  gsum2d2  19949  dprdub  20002  dprdss  20006  dprddisj2  20016  pgpfac1lem3  20054  subrngmre  20539  subrguss  20564  subrgmre  20574  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap2  20635  rhmsscmap  20636  rhmsscrnghm  20642  rngcresringcat  20646  funcringcsetc  20651  unitrrg  20680  isdrng2  20720  primefld0cl  20783  primefld1cl  20784  lssssr  20949  lsssssubg  20953  lssmre  20961  lbspss  21077  lspdisj  21123  lbsextlem2  21157  lidl1el  21224  drngnidl  21241  lpiss  21327  zsssubrg  21405  qsssubdrg  21406  cnsubrg  21407  mulgrhm2  21458  znrrg  21545  ocvocv  21651  ocv2ss  21653  ocvin  21654  lsmcss  21672  cssmre  21673  pjcss  21696  lindfrn  21801  sraassab  21848  mhpsubg  22119  evls1maprnss  22343  dmatsgrp  22464  scmatsgrp  22484  scmatsgrp1  22487  m2cpmrngiso  22723  bastg  22931  tgss  22933  tgtop  22938  tgidm  22945  en2top  22950  neisspw  23072  topssnei  23089  neiptopuni  23095  lpss3  23109  clslp  23113  tgrest  23124  ssrest  23141  restntr  23147  ordtbas2  23156  ordtbas  23157  cnss1  23241  cnss2  23242  cnsscnp  23244  cnrest2r  23252  cmpsublem  23364  cmpsub  23365  tgcmp  23366  cmpcld  23367  hauscmplem  23371  cnconn  23387  llyss  23444  nllyss  23445  restnlly  23447  restlly  23448  locfincmp  23491  locfincf  23496  kgenss  23508  kgenidm  23512  llycmpkgen2  23515  1stckgen  23519  kgen2ss  23520  kgencn3  23523  ptbasfi  23546  ptpjopn  23577  txdis  23597  txkgen  23617  xkoptsub  23619  xkopjcn  23621  txconn  23654  qtoptop2  23664  qtopuni  23667  qtopkgen  23675  basqtop  23676  tgqtop  23677  qtopss  23680  qtoprest  23682  qtopomap  23683  qtopcmap  23684  kqsat  23696  kqcldsat  23698  hmphdis  23761  isfild  23823  ssfg  23837  fgss  23838  fgss2  23839  fgfil  23840  fgabs  23844  filconn  23848  fgtr  23855  uzrest  23862  ufilmax  23872  ufileu  23884  filufint  23885  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  flimss2  23937  flimss1  23938  flimclsi  23943  flimcf  23947  flimsncls  23951  fclssscls  23983  fclsss1  23987  fclsss2  23988  fclscf  23990  uffclsflim  23996  alexsublem  24009  alexsubALTlem3  24014  ptcmplem2  24018  ptcmplem3  24019  cnextf  24031  efmndtmd  24066  symgtgp  24071  cldsubg  24076  tsmscl  24100  haustsms2  24102  tgptsmscls  24115  tsmsxp  24120  restutop  24202  ustuqtop4  24209  utop2nei  24215  utop3cls  24216  ucncn  24249  xblss2ps  24366  xblss2  24367  xrsblre  24777  xrsmopn  24778  recld2  24780  zdis  24782  icccmplem2  24789  cncfss  24866  cnheiborlem  24921  htpycn  24940  phtpyhtpy  24949  pi1blem  25006  cphsscph  25218  cfilfcls  25241  iscmet3lem2  25259  iscmet2  25261  caussi  25264  equivcfil  25266  lmcau  25280  metsscmetcld  25282  hlhil  25410  ivthicc  25425  ovoliunnul  25474  ovolicopnf  25491  uniioombllem3  25552  dyadmbllem  25566  volsup2  25572  vitalilem2  25576  itg1addlem4  25666  itg10a  25677  itg1ge0a  25678  mbfi1fseqlem4  25685  itg2gt0  25727  limciun  25861  perfdvf  25870  cpnord  25902  dvcj  25917  dvlip2  25962  dvivth  25977  dvne0  25978  dvcnvre  25986  ply1lpir  26147  plyco0  26157  plyexmo  26279  abelth  26406  efif1o  26510  logno1  26600  efopnlem2  26621  loglesqrt  26725  lgamcvg2  27018  ppisval  27067  ppinprm  27115  chtnprm  27117  fsumvma  27176  dchrfi  27218  chtppilimlem2  27437  chebbnd2  27440  vmadivsumb  27446  rplogsumlem2  27448  dchrisumlem2  27453  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  selbergb  27512  selberg2b  27515  selberg3lem1  27520  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  oldssmade  27859  ltslpss  27900  noseqrdgfn  28298  n0ssoldg  28345  peano5uzs  28396  uhgredgss  29200  usgruspgrb  29252  uhgrissubgr  29344  uhgrspansubgrlem  29359  uhgrspan1  29372  cusgredg  29493  usgredgsscusgredg  29528  ococss  31364  shsub1  31395  shless  31430  shmodsi  31460  pjhth  31464  spansnss  31642  spanpr  31651  spansnm0i  31721  pjjsi  31771  sumdmdii  32486  sumdmdlem  32489  sumdmdlem2  32490  cdj3lem1  32505  abrexss  32582  fnpreimac  32743  rnmposs  32746  uzssico  32857  ssnnssfz  32860  pwrssmgc  33060  pmtrcnel  33150  cycpmrn  33204  cyc3evpm  33211  cycpmgcl  33214  elrgspnlem1  33303  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem2  33309  fldgensdrg  33375  ringlsmss1  33456  ringlsmss2  33457  prmidlssidl  33505  mxidlirredi  33531  drngmxidl  33537  drngmxidlr  33538  1arithidomlem1  33595  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  ply1mulrtss  33642  esplyfvaln  33718  dimkerim  33771  extdg1id  33810  irngss  33831  irngssv  33832  algextdeglem8  33868  constrsscn  33884  constrsslem  33885  constrsdrg  33919  crefss  33993  cmpcref  33994  zarmxt1  34024  tpr2rico  34056  esumrnmpt2  34212  esumpcvgval  34222  ldsysgenld  34304  sigapildsys  34306  ldgenpisys  34310  cldssbrsiga  34331  measdivcstALTV  34369  mbfmcnt  34412  oddpwdc  34498  eulerpartlemgs2  34524  reprpmtf1o  34770  bnj1033  35111  bnj1398  35176  trssfir1om  35255  r1omhfb  35256  trssfir1omregs  35280  r1omhfbregs  35281  sconnpi1  35421  cvmscld  35455  cvmliftlem15  35480  satfrnmapom  35552  dfon2lem6  35968  fnessref  36539  fgmin  36552  tailfb  36559  dissneqlem  37656  icoreresf  37668  rdglimss  37693  finxpreclem6  37712  lindsenlbs  37936  poimirlem11  37952  poimirlem12  37953  sstotbnd3  38097  prdstotbnd  38115  cntotbnd  38117  ismtyhmeo  38126  1idl  38347  disjdmqsss  39226  lshpdisj  39433  lssats  39458  lkrin  39610  glbconxN  39824  paddss1  40263  paddss2  40264  paddasslem16  40281  paddidm  40287  pmodlem2  40293  pmapjoin  40298  pmapjat1  40299  pclfinN  40346  pclfinclN  40396  diasslssN  41505  dia2dimlem12  41521  dihsslss  41722  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  zndvdchrrhm  42412  dvrelog2  42503  dvrelog3  42504  aks4d1p3  42517  aks4d1p4  42518  aks4d1p5  42519  aks4d1p7  42522  aks4d1p8  42526  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  hashscontpow1  42560  aks6d1c4  42563  sticksstones3  42587  aks6d1c6lem3  42611  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  rhmqusspan  42624  unitscyglem1  42634  unitscyglem4  42637  eldiophss  43206  rencldnfilem  43248  pellexlem5  43261  pell14qrss1234  43284  pell1qrss14  43296  pellfundre  43309  pellfundge  43310  pellfundlb  43312  pellfundglb  43313  harinf  43462  proot1hash  43623  safesnsupfiss  43842  intabssd  43946  ss2iundf  44086  ov2ssiunov2  44127  clsk1indlem3  44470  radcnvrat  44741  nznngen  44743  trsspwALT3  45246  sspwimpALT2  45354  refsumcn  45461  iinssf  45568  icoiccdif  45954  icccncfext  46315  stoweidlem27  46455  stoweidlem46  46474  stoweidlem57  46485  fourierdlem40  46575  fourierdlem78  46612  ffnafv  47619  iccpartrn  47890  sprsymrelfvlem  47950  sprsymrelf1lem  47951  clnbgrssedg  48317  stgrusgra  48435  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  ssnn0ssfz  48825  lincolss  48910  lcoss  48912  lcosslsp  48914  iunord  50151