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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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  4769  uniss  4895  intss1  4943  intmin  4948  intssuni  4950  iinssiun  4985  iunss1  4986  iinss1  4987  ss2iun  4990  ssiun  5026  ssiun2  5027  iinss  5036  iinss2  5037  iunxdif3  5075  sspwb  5434  pwssun  5555  relop  5841  dmss  5893  dmcosseq  5967  dmcosseqOLD  5968  imadifssran  6151  ssrnres  6178  sossfld  6186  predtrss  6322  preddowncl  6332  tron  6386  tz7.7  6389  funimassd  6955  dffv2  6984  chfnrn  7049  fvn0ssdmfun  7074  fveqdmss  7078  dff3  7100  ffnfv  7119  f1imass  7266  ssorduni  7781  onint  7792  limsssuc  7853  limuni3  7855  limomss  7874  fo1stres  8022  fo2ndres  8023  fo2ndf  8128  fnse  8140  ressuppssdif  8192  suppss  8201  reldmtpos  8241  fprlem2  8308  onfununi  8363  smoiun  8383  smocdmdom  8390  tz7.48-1  8465  tz7.49  8467  oaass  8581  cofon1  8692  cofon2  8693  qsss  8800  uniinqs  8819  pmss12g  8891  mapss  8911  ixpssmap2g  8949  ixpssmapg  8950  pssnn  9190  fineqv  9281  finnzfsuppd  9395  ssfii  9441  dffi2  9445  oismo  9562  unxpwdom2  9610  inf3lemd  9649  inf3lem1  9650  inf3lem6  9655  cantnflem3  9713  cantnf  9715  cnfcom3lem  9725  onssr1  9853  rankunb  9872  tcrank  9906  harcard  10000  carduni  10003  infxpenlem  10035  infpwfien  10084  dfac12r  10169  ackbij2lem1  10240  ackbij1lem18  10258  isfin1-3  10408  fin1a2lem11  10432  fin1a2lem13  10434  zorn2lem4  10521  zorn2lem5  10522  ttukeylem6  10536  ttukeylem7  10537  fpwwe2lem10  10662  fpwwe2lem11  10663  fpwwe2  10665  wunr1om  10741  wunom  10742  tskr1om  10789  tskr1om2  10790  tskxpss  10794  tskcard  10803  tskuni  10805  grothomex  10851  genpss  11026  distrlem1pr  11047  distrlem5pr  11049  ltexprlem2  11059  ltexprlem6  11063  ltexprlem7  11064  reclem3pr  11071  reclem4pr  11072  supaddc  12217  supadd  12218  supmul1  12219  supmullem2  12221  peano5uzi  12690  uzss  12883  ixxdisj  13384  ixxss1  13387  ixxss2  13388  ixxss12  13389  ixxub  13390  ixxlb  13391  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  14543  rtrclreclem3  15082  isercoll  15687  summolem2a  15734  fsumcvg3  15748  fsum2dlem  15789  fsumcom2  15793  qshash  15846  prodmolem2a  15953  fprod2dlem  15999  fprodcom2  16003  bitsfzo  16455  1arith  16948  vdwlem2  17003  vdwlem6  17007  vdwlem8  17009  ramtlecl  17021  prmgaplem3  17074  prmgaplem4  17075  monhom  17751  epihom  17758  funcsetcres2  18110  funcestrcsetclem8  18163  funcsetcestrclem8  18178  psdmrn  18588  gsumwspan  18829  frmdss2  18846  sursubmefmnd  18879  injsubmefmnd  18880  trivsubgsnd  19142  ssnmz  19154  trivnsgd  19160  kerf1ghm  19235  conjnmz  19240  symgvalstruct  19383  symgvalstructOLD  19384  gex1  19578  sylow2alem1  19604  lsmless1x  19631  lsmless2x  19632  lsmub1x  19633  lsmub2x  19634  lsmmod  19662  lsmdisj2  19669  efgrelexlemb  19737  efgcpbllemb  19742  cntzcmn  19827  gsum2d2  19961  dprdub  20014  dprdss  20018  dprddisj2  20028  pgpfac1lem3  20066  subrngmre  20531  subrguss  20556  subrgmre  20566  rnghmsscmap2  20598  rnghmsscmap  20599  funcrngcsetc  20609  funcrngcsetcALT  20610  rhmsscmap2  20627  rhmsscmap  20628  rhmsscrnghm  20634  rngcresringcat  20638  funcringcsetc  20643  unitrrg  20672  isdrng2  20712  primefld0cl  20776  primefld1cl  20777  lssssr  20921  lsssssubg  20925  lssmre  20933  lbspss  21050  lspdisj  21096  lbsextlem2  21130  lidl1el  21199  drngnidl  21216  lpiss  21302  zsssubrg  21406  qsssubdrg  21407  cnsubrg  21408  mulgrhm2  21452  znrrg  21539  ocvocv  21644  ocv2ss  21646  ocvin  21647  lsmcss  21665  cssmre  21666  pjcss  21691  lindfrn  21796  sraassab  21843  mhpsubg  22106  evls1maprnss  22331  dmatsgrp  22454  scmatsgrp  22474  scmatsgrp1  22477  m2cpmrngiso  22713  bastg  22921  tgss  22923  tgtop  22928  tgidm  22935  en2top  22940  neisspw  23062  topssnei  23079  neiptopuni  23085  lpss3  23099  clslp  23103  tgrest  23114  ssrest  23131  restntr  23137  ordtbas2  23146  ordtbas  23147  cnss1  23231  cnss2  23232  cnsscnp  23234  cnrest2r  23242  cmpsublem  23354  cmpsub  23355  tgcmp  23356  cmpcld  23357  hauscmplem  23361  cnconn  23377  llyss  23434  nllyss  23435  restnlly  23437  restlly  23438  locfincmp  23481  locfincf  23486  kgenss  23498  kgenidm  23502  llycmpkgen2  23505  1stckgen  23509  kgen2ss  23510  kgencn3  23513  ptbasfi  23536  ptpjopn  23567  txdis  23587  txkgen  23607  xkoptsub  23609  xkopjcn  23611  txconn  23644  qtoptop2  23654  qtopuni  23657  qtopkgen  23665  basqtop  23666  tgqtop  23667  qtopss  23670  qtoprest  23672  qtopomap  23673  qtopcmap  23674  kqsat  23686  kqcldsat  23688  hmphdis  23751  isfild  23813  ssfg  23827  fgss  23828  fgss2  23829  fgfil  23830  fgabs  23834  filconn  23838  fgtr  23845  uzrest  23852  ufilmax  23862  ufileu  23874  filufint  23875  rnelfm  23908  fmfnfmlem2  23910  fmfnfmlem4  23912  flimss2  23927  flimss1  23928  flimclsi  23933  flimcf  23937  flimsncls  23941  fclssscls  23973  fclsss1  23977  fclsss2  23978  fclscf  23980  uffclsflim  23986  alexsublem  23999  alexsubALTlem3  24004  ptcmplem2  24008  ptcmplem3  24009  cnextf  24021  efmndtmd  24056  symgtgp  24061  cldsubg  24066  tsmscl  24090  haustsms2  24092  tgptsmscls  24105  tsmsxp  24110  restutop  24193  ustuqtop4  24200  utop2nei  24206  utop3cls  24207  ucncn  24240  xblss2ps  24357  xblss2  24358  xrsblre  24770  xrsmopn  24771  recld2  24773  zdis  24775  icccmplem2  24782  cncfss  24862  cnheiborlem  24923  htpycn  24942  phtpyhtpy  24951  pi1blem  25009  cphsscph  25222  cfilfcls  25245  iscmet3lem2  25263  iscmet2  25265  caussi  25268  equivcfil  25270  lmcau  25284  metsscmetcld  25286  hlhil  25414  ivthicc  25430  ovoliunnul  25479  ovolicopnf  25496  uniioombllem3  25557  dyadmbllem  25571  volsup2  25577  vitalilem2  25581  itg1addlem4  25671  itg10a  25682  itg1ge0a  25683  mbfi1fseqlem4  25690  itg2gt0  25732  limciun  25866  perfdvf  25875  cpnord  25908  dvcj  25925  dvlip2  25971  dvivth  25986  dvne0  25987  dvcnvre  25995  ply1lpir  26158  plyco0  26168  plyexmo  26292  abelth  26422  efif1o  26525  logno1  26615  efopnlem2  26636  loglesqrt  26741  lgamcvg2  27035  ppisval  27084  ppinprm  27132  chtnprm  27134  fsumvma  27194  dchrfi  27236  chtppilimlem2  27455  chebbnd2  27458  vmadivsumb  27464  rplogsumlem2  27466  dchrisumlem2  27471  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selbergb  27530  selberg2b  27533  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrlog2bndlem2  27559  pntrlog2bndlem4  27561  oldssmade  27853  sltlpss  27882  noseqrdgfn  28249  peano5uzs  28327  uhgredgss  29077  usgruspgrb  29129  uhgrissubgr  29221  uhgrspansubgrlem  29236  uhgrspan1  29249  cusgredg  29370  usgredgsscusgredg  29406  ococss  31241  shsub1  31272  shless  31307  shmodsi  31337  pjhth  31341  spansnss  31519  spanpr  31528  spansnm0i  31598  pjjsi  31648  sumdmdii  32363  sumdmdlem  32366  sumdmdlem2  32367  cdj3lem1  32382  abrexss  32460  fnpreimac  32617  rnmposs  32620  unifi3  32660  uzssico  32730  ssnnssfz  32733  pwrssmgc  32934  pmtrcnel  33053  cycpmrn  33107  cyc3evpm  33114  cycpmgcl  33117  elrgspnlem1  33190  elrgspnlem3  33192  elrgspnlem4  33193  elrgspnsubrunlem2  33196  fldgensdrg  33261  ringlsmss1  33364  ringlsmss2  33365  prmidlssidl  33413  mxidlirredi  33439  drngmxidl  33445  drngmxidlr  33446  1arithidomlem1  33503  1arithidom  33505  1arithufdlem2  33513  1arithufdlem3  33514  1arithufdlem4  33515  dfufd2lem  33517  ply1mulrtss  33546  dimkerim  33618  extdg1id  33658  irngss  33679  irngssv  33680  algextdeglem8  33709  constrsscn  33725  constrsslem  33726  constrsdrg  33760  crefss  33823  cmpcref  33824  zarmxt1  33854  tpr2rico  33886  esumrnmpt2  34044  esumpcvgval  34054  ldsysgenld  34136  sigapildsys  34138  ldgenpisys  34142  cldssbrsiga  34163  measdivcstALTV  34201  mbfmcnt  34245  oddpwdc  34331  eulerpartlemgs2  34357  reprpmtf1o  34616  bnj1033  34958  bnj1398  35023  sconnpi1  35219  cvmscld  35253  cvmliftlem15  35278  satfrnmapom  35350  dfon2lem6  35764  fnessref  36333  fgmin  36346  tailfb  36353  dissneqlem  37316  icoreresf  37328  rdglimss  37353  finxpreclem6  37372  lindsenlbs  37597  poimirlem11  37613  poimirlem12  37614  sstotbnd3  37758  prdstotbnd  37776  cntotbnd  37778  ismtyhmeo  37787  1idl  38008  disjdmqsss  38778  lshpdisj  38963  lssats  38988  lkrin  39140  glbconxN  39355  paddss1  39794  paddss2  39795  paddasslem16  39812  paddidm  39818  pmodlem2  39824  pmapjoin  39829  pmapjat1  39830  pclfinN  39877  pclfinclN  39927  diasslssN  41036  dia2dimlem12  41052  dihsslss  41253  baerlem3lem2  41687  baerlem5alem2  41688  baerlem5blem2  41689  zndvdchrrhm  41947  dvrelog2  42040  dvrelog3  42041  aks4d1p3  42054  aks4d1p4  42055  aks4d1p5  42056  aks4d1p7  42059  aks4d1p8  42063  primrootsunit1  42073  primrootscoprmpow  42075  primrootscoprbij  42078  hashscontpow1  42097  aks6d1c4  42100  sticksstones3  42124  aks6d1c6lem3  42148  aks6d1c6isolem2  42151  aks6d1c6lem5  42153  rhmqusspan  42161  unitscyglem1  42171  unitscyglem4  42174  ss2ab1  42233  eldiophss  42763  rencldnfilem  42809  pellexlem5  42822  pell14qrss1234  42845  pell1qrss14  42857  pellfundre  42870  pellfundge  42871  pellfundlb  42873  pellfundglb  42874  harinf  43024  proot1hash  43185  safesnsupfiss  43405  intabssd  43509  ss2iundf  43649  ov2ssiunov2  43690  clsk1indlem3  44033  radcnvrat  44305  nznngen  44307  trsspwALT3  44812  sspwimpALT2  44920  refsumcn  45007  iinssf  45115  icoiccdif  45509  icccncfext  45874  stoweidlem27  46014  stoweidlem46  46033  stoweidlem57  46044  fourierdlem40  46134  fourierdlem78  46171  ffnafv  47156  iccpartrn  47390  sprsymrelfvlem  47450  sprsymrelf1lem  47451  clnbgrssedg  47800  stgrusgra  47899  rhmsubcALTVlem4  48173  funcringcsetcALTV2lem8  48186  funcringcsetclem8ALTV  48209  ssnn0ssfz  48238  lincolss  48324  lcoss  48326  lcosslsp  48328  iunord  49290