Theorem ssrdv 3922

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

Syntax hints:   → wi 4  ∀wal 1546   ∈ wcel 2121   ⊆ wss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-ss 3901

This theorem is referenced by:  eqelssd  3937  ss2abim  3993  ss2abdv  3998  sscon  4075  ssdif  4076  unss1  4116  ssrin  4172  eq0rdvALT  4338  sspw  4542  elpwdifsn  4724  uniss  4848  intss1  4895  intmin  4900  intssuni  4902  iinssiun  4937  iunss1  4938  iinss1  4939  ss2iun  4942  ssiun  4978  ssiun2  4979  iinss  4988  iinss2  4989  iunxdif3  5026  sspwb  5390  pwssun  5512  relop  5794  dmss  5850  dmcosseq  5926  dmcosseqOLD  5927  dmcosseqOLDOLD  5928  imadifssran  6105  ssrnres  6132  sossfld  6140  predtrss  6276  preddowncl  6286  tron  6336  tz7.7  6339  funimassd  6896  dffv2  6925  chfnrn  6993  fvn0ssdmfun  7018  fveqdmss  7022  dff3  7044  ffnfv  7063  f1imass  7211  ssorduni  7725  onint  7736  limsssuc  7793  limuni3  7795  limomss  7814  fo1stres  7959  fo2ndres  7960  fo2ndf  8062  fnse  8075  ressuppssdif  8127  suppss  8136  reldmtpos  8176  fprlem2  8244  onfununi  8274  smoiun  8294  smocdmdom  8301  tz7.48-1  8376  tz7.49  8378  oaass  8490  cofon1  8602  cofon2  8603  qsss  8716  uniinqs  8738  pmss12g  8811  mapss  8831  ixpssmap2g  8869  ixpssmapg  8870  pssnn  9097  fineqv  9171  unifi3  9266  finnzfsuppd  9280  ssfii  9326  dffi2  9330  oismo  9449  unxpwdom2  9497  inf3lemd  9543  inf3lem1  9544  inf3lem6  9549  cantnflem3  9607  cantnf  9609  cnfcom3lem  9619  onssr1  9750  rankunb  9769  tcrank  9803  harcard  9897  carduni  9900  infxpenlem  9930  infpwfien  9979  dfac12r  10064  ackbij2lem1  10135  ackbij1lem18  10153  isfin1-3  10304  fin1a2lem11  10328  fin1a2lem13  10330  zorn2lem4  10417  zorn2lem5  10418  ttukeylem6  10432  ttukeylem7  10433  fpwwe2lem10  10559  fpwwe2lem11  10560  fpwwe2  10562  wunr1om  10638  wunom  10639  tskr1om  10686  tskr1om2  10687  tskxpss  10691  tskcard  10700  tskuni  10702  grothomex  10748  genpss  10923  distrlem1pr  10944  distrlem5pr  10946  ltexprlem2  10956  ltexprlem6  10960  ltexprlem7  10961  reclem3pr  10968  reclem4pr  10969  supaddc  12118  supadd  12119  supmul1  12120  supmullem2  12122  peano5uzi  12613  uzss  12806  ixxdisj  13308  ixxss1  13311  ixxss2  13312  ixxss12  13313  ixxub  13314  ixxlb  13315  iocssre  13375  icossre  13376  iccssre  13377  icodisj  13424  fzss1  13512  fzss2  13513  ssfzunsnext  13518  fzosplit  13642  fzouzsplit  13644  ssfzo12bi  13711  ssnn0fi  13942  fsuppmapnn0fiub  13948  suppssfz  13951  sswrd  14479  rtrclreclem3  15017  isercoll  15625  summolem2a  15672  fsumcvg3  15686  fsum2dlem  15727  fsumcom2  15731  qshash  15785  prodmolem2a  15894  fprod2dlem  15940  fprodcom2  15944  bitsfzo  16399  1arith  16893  vdwlem2  16948  vdwlem6  16952  vdwlem8  16954  ramtlecl  16966  prmgaplem3  17019  prmgaplem4  17020  monhom  17697  epihom  17704  funcsetcres2  18055  funcestrcsetclem8  18108  funcsetcestrclem8  18123  psdmrn  18534  chnrss  18576  chndss  18577  gsumwspan  18809  frmdss2  18826  sursubmefmnd  18859  injsubmefmnd  18860  trivsubgsnd  19124  ssnmz  19136  trivnsgd  19142  kerf1ghm  19216  conjnmz  19221  symgvalstruct  19366  gex1  19560  sylow2alem1  19586  lsmless1x  19613  lsmless2x  19614  lsmub1x  19615  lsmub2x  19616  lsmmod  19644  lsmdisj2  19651  efgrelexlemb  19719  efgcpbllemb  19724  cntzcmn  19809  gsum2d2  19943  dprdub  19996  dprdss  20000  dprddisj2  20010  pgpfac1lem3  20048  subrngmre  20537  subrguss  20562  subrgmre  20572  rnghmsscmap2  20604  rnghmsscmap  20605  funcrngcsetc  20615  funcrngcsetcALT  20616  rhmsscmap2  20633  rhmsscmap  20634  rhmsscrnghm  20640  rngcresringcat  20644  funcringcsetc  20649  unitrrg  20678  isdrng2  20718  primefld0cl  20781  primefld1cl  20782  lssssr  20947  lsssssubg  20951  lssmre  20959  lbspss  21075  lspdisj  21121  lbsextlem2  21155  lidl1el  21222  drngnidl  21239  lpiss  21325  zsssubrg  21403  qsssubdrg  21404  cnsubrg  21405  mulgrhm2  21456  znrrg  21543  ocvocv  21649  ocv2ss  21651  ocvin  21652  lsmcss  21670  cssmre  21671  pjcss  21694  lindfrn  21799  sraassab  21846  mhpsubg  22144  evls1maprnss  22367  dmatsgrp  22485  scmatsgrp  22505  scmatsgrp1  22508  m2cpmrngiso  22744  bastg  22952  tgss  22954  tgtop  22959  tgidm  22966  en2top  22971  neisspw  23093  topssnei  23110  neiptopuni  23116  lpss3  23130  clslp  23134  tgrest  23145  ssrest  23162  restntr  23168  ordtbas2  23177  ordtbas  23178  cnss1  23262  cnss2  23263  cnsscnp  23265  cnrest2r  23273  cmpsublem  23385  cmpsub  23386  tgcmp  23387  cmpcld  23388  hauscmplem  23392  cnconn  23408  llyss  23465  nllyss  23466  restnlly  23468  restlly  23469  locfincmp  23512  locfincf  23517  kgenss  23529  kgenidm  23533  llycmpkgen2  23536  1stckgen  23540  kgen2ss  23541  kgencn3  23544  ptbasfi  23567  ptpjopn  23598  txdis  23618  txkgen  23638  xkoptsub  23640  xkopjcn  23642  txconn  23675  qtoptop2  23685  qtopuni  23688  qtopkgen  23696  basqtop  23697  tgqtop  23698  qtopss  23701  qtoprest  23703  qtopomap  23704  qtopcmap  23705  kqsat  23717  kqcldsat  23719  hmphdis  23782  isfild  23844  ssfg  23858  fgss  23859  fgss2  23860  fgfil  23861  fgabs  23865  filconn  23869  fgtr  23876  uzrest  23883  ufilmax  23893  ufileu  23905  filufint  23906  rnelfm  23939  fmfnfmlem2  23941  fmfnfmlem4  23943  flimss2  23958  flimss1  23959  flimclsi  23964  flimcf  23968  flimsncls  23972  fclssscls  24004  fclsss1  24008  fclsss2  24009  fclscf  24011  uffclsflim  24017  alexsublem  24030  alexsubALTlem3  24035  ptcmplem2  24039  ptcmplem3  24040  cnextf  24052  efmndtmd  24087  symgtgp  24092  cldsubg  24097  tsmscl  24121  haustsms2  24123  tgptsmscls  24136  tsmsxp  24141  restutop  24223  ustuqtop4  24230  utop2nei  24236  utop3cls  24237  ucncn  24270  xblss2ps  24387  xblss2  24388  xrsblre  24798  xrsmopn  24799  recld2  24801  zdis  24803  icccmplem2  24810  cncfss  24887  cnheiborlem  24942  htpycn  24961  phtpyhtpy  24970  pi1blem  25027  cphsscph  25239  cfilfcls  25262  iscmet3lem2  25280  iscmet2  25282  caussi  25285  equivcfil  25287  lmcau  25301  metsscmetcld  25303  hlhil  25431  ivthicc  25446  ovoliunnul  25495  ovolicopnf  25512  uniioombllem3  25573  dyadmbllem  25587  volsup2  25593  vitalilem2  25597  itg1addlem4  25687  itg10a  25698  itg1ge0a  25699  mbfi1fseqlem4  25706  itg2gt0  25748  limciun  25882  perfdvf  25891  cpnord  25923  dvcj  25938  dvlip2  25983  dvivth  25998  dvne0  25999  dvcnvre  26007  ply1lpir  26168  plyco0  26178  plyexmo  26300  abelth  26427  efif1o  26531  logno1  26621  efopnlem2  26642  loglesqrt  26746  lgamcvg2  27039  ppisval  27088  ppinprm  27136  chtnprm  27138  fsumvma  27197  dchrfi  27239  chtppilimlem2  27458  chebbnd2  27461  vmadivsumb  27467  rplogsumlem2  27469  dchrisumlem2  27474  vmalogdivsum2  27522  vmalogdivsum  27523  2vmadivsumlem  27524  selbergb  27533  selberg2b  27536  selberg3lem1  27541  selberg3lem2  27542  selberg3  27543  selberg4lem1  27544  selberg4  27545  pntrlog2bndlem2  27562  pntrlog2bndlem4  27564  oldssmade  27879  ltslpss  27920  noseqrdgfn  28318  n0ssoldg  28365  peano5uzs  28416  uhgredgss  29220  usgruspgrb  29272  uhgrissubgr  29364  uhgrspansubgrlem  29379  uhgrspan1  29392  cusgredg  29513  usgredgsscusgredg  29548  ococss  31384  shsub1  31415  shless  31450  shmodsi  31480  pjhth  31484  spansnss  31662  spanpr  31671  spansnm0i  31741  pjjsi  31791  sumdmdii  32506  sumdmdlem  32509  sumdmdlem2  32510  cdj3lem1  32525  abrexss  32602  fnpreimac  32764  rnmposs  32767  uzssico  32878  ssnnssfz  32881  pwrssmgc  33081  pmtrcnel  33172  cycpmrn  33226  cyc3evpm  33233  cycpmgcl  33236  elrgspnlem1  33325  elrgspnlem3  33327  elrgspnlem4  33328  elrgspnsubrunlem2  33331  fldgensdrg  33400  ringlsmss1  33481  ringlsmss2  33482  prmidlssidl  33530  mxidlirredi  33556  drngmxidl  33562  drngmxidlr  33563  1arithidomlem1  33628  1arithidom  33630  1arithufdlem2  33638  1arithufdlem3  33639  1arithufdlem4  33640  dfufd2lem  33642  ply1mulrtss  33675  esplyfvaln  33768  dimkerim  33821  extdg1id  33860  irngss  33881  irngssv  33882  algextdeglem8  33918  constrsscn  33934  constrsslem  33935  constrsdrg  33969  crefss  34043  cmpcref  34044  zarmxt1  34074  tpr2rico  34106  esumrnmpt2  34262  esumpcvgval  34272  ldsysgenld  34354  sigapildsys  34356  ldgenpisys  34360  cldssbrsiga  34381  measdivcstALTV  34419  mbfmcnt  34462  oddpwdc  34548  eulerpartlemgs2  34574  reprpmtf1o  34820  bnj1033  35164  bnj1398  35229  trssfir1om  35305  r1omhfb  35306  trssfir1omregs  35330  r1omhfbregs  35331  sconnpi1  35480  cvmscld  35514  cvmliftlem15  35539  satfrnmapom  35611  dfon2lem6  36027  fnessref  36598  fgmin  36611  tailfb  36618  dissneqlem  37715  icoreresf  37727  rdglimss  37752  finxpreclem6  37771  lindsenlbs  37995  poimirlem11  38011  poimirlem12  38012  sstotbnd3  38156  prdstotbnd  38174  cntotbnd  38176  ismtyhmeo  38185  1idl  38406  disjdmqsss  39285  lshpdisj  39492  lssats  39517  lkrin  39669  glbconxN  39883  paddss1  40322  paddss2  40323  paddasslem16  40340  paddidm  40346  pmodlem2  40352  pmapjoin  40357  pmapjat1  40358  pclfinN  40405  pclfinclN  40455  diasslssN  41564  dia2dimlem12  41580  dihsslss  41781  baerlem3lem2  42215  baerlem5alem2  42216  baerlem5blem2  42217  zndvdchrrhm  42471  dvrelog2  42562  dvrelog3  42563  aks4d1p3  42576  aks4d1p4  42577  aks4d1p5  42578  aks4d1p7  42581  aks4d1p8  42585  primrootsunit1  42595  primrootscoprmpow  42597  primrootscoprbij  42600  hashscontpow1  42619  aks6d1c4  42622  sticksstones3  42646  aks6d1c6lem3  42670  aks6d1c6isolem2  42673  aks6d1c6lem5  42675  rhmqusspan  42683  unitscyglem1  42693  unitscyglem4  42696  eldiophss  43236  rencldnfilem  43278  pellexlem5  43291  pell14qrss1234  43314  pell1qrss14  43326  pellfundre  43339  pellfundge  43340  pellfundlb  43342  pellfundglb  43343  harinf  43492  proot1hash  43653  safesnsupfiss  43872  intabssd  43976  ss2iundf  44116  ov2ssiunov2  44157  clsk1indlem3  44500  radcnvrat  44771  nznngen  44773  trsspwALT3  45276  sspwimpALT2  45384  refsumcn  45491  iinssf  45597  icoiccdif  45981  icccncfext  46342  stoweidlem27  46482  stoweidlem46  46501  stoweidlem57  46512  fourierdlem40  46602  fourierdlem78  46639  ffnafv  47646  iccpartrn  47917  sprsymrelfvlem  47977  sprsymrelf1lem  47978  clnbgrssedg  48344  stgrusgra  48462  rhmsubcALTVlem4  48787  funcringcsetcALTV2lem8  48800  funcringcsetclem8ALTV  48823  ssnn0ssfz  48852  lincolss  48937  lcoss  48939  lcosslsp  48941  iunord  50178