Theorem ssrdv 3952

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

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

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 3931

This theorem is referenced by:  eqelssd  3968  ss2abdv  4029  sscon  4106  ssdif  4107  unss1  4148  ssrin  4205  eq0rdvALT  4371  sspw  4574  elpwdifsn  4753  uniss  4879  intss1  4927  intmin  4932  intssuni  4934  iinssiun  4969  iunss1  4970  iinss1  4971  ss2iun  4974  ssiun  5010  ssiun2  5011  iinss  5020  iinss2  5021  iunxdif3  5059  sspwb  5409  pwssun  5530  relop  5814  dmss  5866  dmcosseq  5940  dmcosseqOLD  5941  imadifssran  6124  ssrnres  6151  sossfld  6159  predtrss  6295  preddowncl  6305  tron  6355  tz7.7  6358  funimassd  6927  dffv2  6956  chfnrn  7021  fvn0ssdmfun  7046  fveqdmss  7050  dff3  7072  ffnfv  7091  f1imass  7239  ssorduni  7755  onint  7766  limsssuc  7826  limuni3  7828  limomss  7847  fo1stres  7994  fo2ndres  7995  fo2ndf  8100  fnse  8112  ressuppssdif  8164  suppss  8173  reldmtpos  8213  fprlem2  8280  onfununi  8310  smoiun  8330  smocdmdom  8337  tz7.48-1  8411  tz7.49  8413  oaass  8525  cofon1  8636  cofon2  8637  qsss  8749  uniinqs  8770  pmss12g  8842  mapss  8862  ixpssmap2g  8900  ixpssmapg  8901  pssnn  9132  fineqv  9210  finnzfsuppd  9324  ssfii  9370  dffi2  9374  oismo  9493  unxpwdom2  9541  inf3lemd  9580  inf3lem1  9581  inf3lem6  9586  cantnflem3  9644  cantnf  9646  cnfcom3lem  9656  onssr1  9784  rankunb  9803  tcrank  9837  harcard  9931  carduni  9934  infxpenlem  9966  infpwfien  10015  dfac12r  10100  ackbij2lem1  10171  ackbij1lem18  10189  isfin1-3  10339  fin1a2lem11  10363  fin1a2lem13  10365  zorn2lem4  10452  zorn2lem5  10453  ttukeylem6  10467  ttukeylem7  10468  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2  10596  wunr1om  10672  wunom  10673  tskr1om  10720  tskr1om2  10721  tskxpss  10725  tskcard  10734  tskuni  10736  grothomex  10782  genpss  10957  distrlem1pr  10978  distrlem5pr  10980  ltexprlem2  10990  ltexprlem6  10994  ltexprlem7  10995  reclem3pr  11002  reclem4pr  11003  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  peano5uzi  12623  uzss  12816  ixxdisj  13321  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  iocssre  13388  icossre  13389  iccssre  13390  icodisj  13437  fzss1  13524  fzss2  13525  ssfzunsnext  13530  fzosplit  13653  fzouzsplit  13655  ssfzo12bi  13722  ssnn0fi  13950  fsuppmapnn0fiub  13956  suppssfz  13959  sswrd  14487  rtrclreclem3  15026  isercoll  15634  summolem2a  15681  fsumcvg3  15695  fsum2dlem  15736  fsumcom2  15740  qshash  15793  prodmolem2a  15900  fprod2dlem  15946  fprodcom2  15950  bitsfzo  16405  1arith  16898  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  ramtlecl  16971  prmgaplem3  17024  prmgaplem4  17025  monhom  17697  epihom  17704  funcsetcres2  18055  funcestrcsetclem8  18108  funcsetcestrclem8  18123  psdmrn  18532  gsumwspan  18773  frmdss2  18790  sursubmefmnd  18823  injsubmefmnd  18824  trivsubgsnd  19086  ssnmz  19098  trivnsgd  19104  kerf1ghm  19179  conjnmz  19184  symgvalstruct  19327  gex1  19521  sylow2alem1  19547  lsmless1x  19574  lsmless2x  19575  lsmub1x  19576  lsmub2x  19577  lsmmod  19605  lsmdisj2  19612  efgrelexlemb  19680  efgcpbllemb  19685  cntzcmn  19770  gsum2d2  19904  dprdub  19957  dprdss  19961  dprddisj2  19971  pgpfac1lem3  20009  subrngmre  20471  subrguss  20496  subrgmre  20506  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap2  20567  rhmsscmap  20568  rhmsscrnghm  20574  rngcresringcat  20578  funcringcsetc  20583  unitrrg  20612  isdrng2  20652  primefld0cl  20715  primefld1cl  20716  lssssr  20860  lsssssubg  20864  lssmre  20872  lbspss  20989  lspdisj  21035  lbsextlem2  21069  lidl1el  21136  drngnidl  21153  lpiss  21239  zsssubrg  21342  qsssubdrg  21343  cnsubrg  21344  mulgrhm2  21388  znrrg  21475  ocvocv  21580  ocv2ss  21582  ocvin  21583  lsmcss  21601  cssmre  21602  pjcss  21625  lindfrn  21730  sraassab  21777  mhpsubg  22040  evls1maprnss  22265  dmatsgrp  22386  scmatsgrp  22406  scmatsgrp1  22409  m2cpmrngiso  22645  bastg  22853  tgss  22855  tgtop  22860  tgidm  22867  en2top  22872  neisspw  22994  topssnei  23011  neiptopuni  23017  lpss3  23031  clslp  23035  tgrest  23046  ssrest  23063  restntr  23069  ordtbas2  23078  ordtbas  23079  cnss1  23163  cnss2  23164  cnsscnp  23166  cnrest2r  23174  cmpsublem  23286  cmpsub  23287  tgcmp  23288  cmpcld  23289  hauscmplem  23293  cnconn  23309  llyss  23366  nllyss  23367  restnlly  23369  restlly  23370  locfincmp  23413  locfincf  23418  kgenss  23430  kgenidm  23434  llycmpkgen2  23437  1stckgen  23441  kgen2ss  23442  kgencn3  23445  ptbasfi  23468  ptpjopn  23499  txdis  23519  txkgen  23539  xkoptsub  23541  xkopjcn  23543  txconn  23576  qtoptop2  23586  qtopuni  23589  qtopkgen  23597  basqtop  23598  tgqtop  23599  qtopss  23602  qtoprest  23604  qtopomap  23605  qtopcmap  23606  kqsat  23618  kqcldsat  23620  hmphdis  23683  isfild  23745  ssfg  23759  fgss  23760  fgss2  23761  fgfil  23762  fgabs  23766  filconn  23770  fgtr  23777  uzrest  23784  ufilmax  23794  ufileu  23806  filufint  23807  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  flimss2  23859  flimss1  23860  flimclsi  23865  flimcf  23869  flimsncls  23873  fclssscls  23905  fclsss1  23909  fclsss2  23910  fclscf  23912  uffclsflim  23918  alexsublem  23931  alexsubALTlem3  23936  ptcmplem2  23940  ptcmplem3  23941  cnextf  23953  efmndtmd  23988  symgtgp  23993  cldsubg  23998  tsmscl  24022  haustsms2  24024  tgptsmscls  24037  tsmsxp  24042  restutop  24125  ustuqtop4  24132  utop2nei  24138  utop3cls  24139  ucncn  24172  xblss2ps  24289  xblss2  24290  xrsblre  24700  xrsmopn  24701  recld2  24703  zdis  24705  icccmplem2  24712  cncfss  24792  cnheiborlem  24853  htpycn  24872  phtpyhtpy  24881  pi1blem  24939  cphsscph  25151  cfilfcls  25174  iscmet3lem2  25192  iscmet2  25194  caussi  25197  equivcfil  25199  lmcau  25213  metsscmetcld  25215  hlhil  25343  ivthicc  25359  ovoliunnul  25408  ovolicopnf  25425  uniioombllem3  25486  dyadmbllem  25500  volsup2  25506  vitalilem2  25510  itg1addlem4  25600  itg10a  25611  itg1ge0a  25612  mbfi1fseqlem4  25619  itg2gt0  25661  limciun  25795  perfdvf  25804  cpnord  25837  dvcj  25854  dvlip2  25900  dvivth  25915  dvne0  25916  dvcnvre  25924  ply1lpir  26087  plyco0  26097  plyexmo  26221  abelth  26351  efif1o  26455  logno1  26545  efopnlem2  26566  loglesqrt  26671  lgamcvg2  26965  ppisval  27014  ppinprm  27062  chtnprm  27064  fsumvma  27124  dchrfi  27166  chtppilimlem2  27385  chebbnd2  27388  vmadivsumb  27394  rplogsumlem2  27396  dchrisumlem2  27401  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  selbergb  27460  selberg2b  27463  selberg3lem1  27468  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  oldssmade  27789  sltlpss  27819  noseqrdgfn  28200  peano5uzs  28292  uhgredgss  29058  usgruspgrb  29110  uhgrissubgr  29202  uhgrspansubgrlem  29217  uhgrspan1  29230  cusgredg  29351  usgredgsscusgredg  29387  ococss  31222  shsub1  31253  shless  31288  shmodsi  31318  pjhth  31322  spansnss  31500  spanpr  31509  spansnm0i  31579  pjjsi  31629  sumdmdii  32344  sumdmdlem  32347  sumdmdlem2  32348  cdj3lem1  32363  abrexss  32441  fnpreimac  32595  rnmposs  32598  unifi3  32636  uzssico  32707  ssnnssfz  32710  pwrssmgc  32926  pmtrcnel  33046  cycpmrn  33100  cyc3evpm  33107  cycpmgcl  33110  elrgspnlem1  33193  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem2  33199  fldgensdrg  33264  ringlsmss1  33367  ringlsmss2  33368  prmidlssidl  33416  mxidlirredi  33442  drngmxidl  33448  drngmxidlr  33449  1arithidomlem1  33506  1arithidom  33508  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  ply1mulrtss  33550  dimkerim  33623  extdg1id  33661  irngss  33682  irngssv  33683  algextdeglem8  33714  constrsscn  33730  constrsslem  33731  constrsdrg  33765  crefss  33839  cmpcref  33840  zarmxt1  33870  tpr2rico  33902  esumrnmpt2  34058  esumpcvgval  34068  ldsysgenld  34150  sigapildsys  34152  ldgenpisys  34156  cldssbrsiga  34177  measdivcstALTV  34215  mbfmcnt  34259  oddpwdc  34345  eulerpartlemgs2  34371  reprpmtf1o  34617  bnj1033  34959  bnj1398  35024  sconnpi1  35226  cvmscld  35260  cvmliftlem15  35285  satfrnmapom  35357  dfon2lem6  35776  fnessref  36345  fgmin  36358  tailfb  36365  dissneqlem  37328  icoreresf  37340  rdglimss  37365  finxpreclem6  37384  lindsenlbs  37609  poimirlem11  37625  poimirlem12  37626  sstotbnd3  37770  prdstotbnd  37788  cntotbnd  37790  ismtyhmeo  37799  1idl  38020  disjdmqsss  38794  lshpdisj  38980  lssats  39005  lkrin  39157  glbconxN  39372  paddss1  39811  paddss2  39812  paddasslem16  39829  paddidm  39835  pmodlem2  39841  pmapjoin  39846  pmapjat1  39847  pclfinN  39894  pclfinclN  39944  diasslssN  41053  dia2dimlem12  41069  dihsslss  41270  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  zndvdchrrhm  41960  dvrelog2  42052  dvrelog3  42053  aks4d1p3  42066  aks4d1p4  42067  aks4d1p5  42068  aks4d1p7  42071  aks4d1p8  42075  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  hashscontpow1  42109  aks6d1c4  42112  sticksstones3  42136  aks6d1c6lem3  42160  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  rhmqusspan  42173  unitscyglem1  42183  unitscyglem4  42186  ss2ab1  42207  eldiophss  42762  rencldnfilem  42808  pellexlem5  42821  pell14qrss1234  42844  pell1qrss14  42856  pellfundre  42869  pellfundge  42870  pellfundlb  42872  pellfundglb  42873  harinf  43023  proot1hash  43184  safesnsupfiss  43404  intabssd  43508  ss2iundf  43648  ov2ssiunov2  43689  clsk1indlem3  44032  radcnvrat  44303  nznngen  44305  trsspwALT3  44809  sspwimpALT2  44917  refsumcn  45024  iinssf  45132  icoiccdif  45522  icccncfext  45885  stoweidlem27  46025  stoweidlem46  46044  stoweidlem57  46055  fourierdlem40  46145  fourierdlem78  46182  ffnafv  47172  iccpartrn  47431  sprsymrelfvlem  47491  sprsymrelf1lem  47492  clnbgrssedg  47841  stgrusgra  47958  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  ssnn0ssfz  48337  lincolss  48423  lcoss  48425  lcosslsp  48427  iunord  49665