Theorem ssrdv 3940

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

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

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

This theorem is referenced by:  eqelssd  3955  ss2abim  4011  ss2abdv  4016  sscon  4094  ssdif  4095  unss1  4135  ssrin  4191  eq0rdvALT  4359  sspw  4563  elpwdifsn  4746  uniss  4870  intss1  4918  intmin  4923  intssuni  4925  iinssiun  4960  iunss1  4961  iinss1  4962  ss2iun  4965  ssiun  5001  ssiun2  5002  iinss  5011  iinss2  5012  iunxdif3  5049  sspwb  5413  pwssun  5535  relop  5818  dmss  5874  dmcosseq  5950  dmcosseqOLD  5951  dmcosseqOLDOLD  5952  imadifssran  6132  ssrnres  6159  sossfld  6167  predtrss  6304  preddowncl  6314  tron  6364  tz7.7  6367  funimassd  6928  dffv2  6957  chfnrn  7025  fvn0ssdmfun  7050  fveqdmss  7054  dff3  7076  ffnfv  7095  f1imass  7243  ssorduni  7757  onint  7768  limsssuc  7825  limuni3  7827  limomss  7846  fo1stres  7991  fo2ndres  7992  fo2ndf  8094  fnse  8107  ressuppssdif  8159  suppss  8168  reldmtpos  8208  fprlem2  8276  onfununi  8306  smoiun  8326  smocdmdom  8333  tz7.48-1  8408  tz7.49  8410  oaass  8524  cofon1  8636  cofon2  8637  qsss  8751  uniinqs  8773  pmss12g  8845  mapss  8865  ixpssmap2g  8903  ixpssmapg  8904  pssnn  9131  fineqv  9205  unifi3  9299  finnzfsuppd  9313  ssfii  9359  dffi2  9363  oismo  9482  unxpwdom2  9530  inf3lemd  9576  inf3lem1  9577  inf3lem6  9582  cantnflem3  9640  cantnf  9642  cnfcom3lem  9652  onssr1  9783  rankunb  9802  tcrank  9836  harcard  9930  carduni  9933  infxpenlem  9963  infpwfien  10012  dfac12r  10097  ackbij2lem1  10168  ackbij1lem18  10186  isfin1-3  10337  fin1a2lem11  10361  fin1a2lem13  10363  zorn2lem4  10450  zorn2lem5  10451  ttukeylem6  10465  ttukeylem7  10466  fpwwe2lem10  10592  fpwwe2lem11  10593  fpwwe2  10595  wunr1om  10671  wunom  10672  tskr1om  10719  tskr1om2  10720  tskxpss  10724  tskcard  10733  tskuni  10735  grothomex  10781  genpss  10956  distrlem1pr  10977  distrlem5pr  10979  ltexprlem2  10989  ltexprlem6  10993  ltexprlem7  10994  reclem3pr  11001  reclem4pr  11002  supaddc  12153  supadd  12154  supmul1  12155  supmullem2  12157  peano5uzi  12656  uzss  12856  ixxdisj  13358  ixxss1  13361  ixxss2  13362  ixxss12  13363  ixxub  13364  ixxlb  13365  iocssre  13425  icossre  13426  iccssre  13427  icodisj  13474  fzss1  13562  fzss2  13563  ssfzunsnext  13568  fzosplit  13692  fzouzsplit  13694  ssfzo12bi  13761  ssnn0fi  13992  fsuppmapnn0fiub  13998  suppssfz  14001  sswrd  14529  rtrclreclem3  15067  isercoll  15686  summolem2a  15733  fsumcvg3  15747  fsum2dlem  15788  fsumcom2  15792  qshash  15846  prodmolem2a  15955  fprod2dlem  16001  fprodcom2  16005  bitsfzo  16460  1arith  16954  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  ramtlecl  17027  prmgaplem3  17080  prmgaplem4  17081  monhom  17759  epihom  17766  funcsetcres2  18117  funcestrcsetclem8  18170  funcsetcestrclem8  18185  psdmrn  18596  chnrss  18638  chndss  18639  gsumwspan  18871  frmdss2  18888  sursubmefmnd  18921  injsubmefmnd  18922  trivsubgsnd  19186  ssnmz  19198  trivnsgd  19204  kerf1ghm  19278  conjnmz  19283  symgvalstruct  19428  gex1  19622  sylow2alem1  19648  lsmless1x  19675  lsmless2x  19676  lsmub1x  19677  lsmub2x  19678  lsmmod  19706  lsmdisj2  19713  efgrelexlemb  19781  efgcpbllemb  19786  cntzcmn  19871  gsum2d2  20005  dprdub  20058  dprdss  20062  dprddisj2  20072  pgpfac1lem3  20110  subrngmre  20599  subrguss  20624  subrgmre  20634  rnghmsscmap2  20666  rnghmsscmap  20667  funcrngcsetc  20677  funcrngcsetcALT  20678  rhmsscmap2  20695  rhmsscmap  20696  rhmsscrnghm  20702  rngcresringcat  20706  funcringcsetc  20711  unitrrg  20740  isdrng2  20780  primefld0cl  20843  primefld1cl  20844  lssssr  21009  lsssssubg  21013  lssmre  21021  lbspss  21137  lspdisj  21183  lbsextlem2  21217  lidl1el  21284  drngnidl  21301  lpiss  21387  zsssubrg  21465  qsssubdrg  21466  cnsubrg  21467  mulgrhm2  21518  znrrg  21605  ocvocv  21711  ocv2ss  21713  ocvin  21714  lsmcss  21732  cssmre  21733  pjcss  21756  lindfrn  21861  sraassab  21908  mhpsubg  22206  evls1maprnss  22429  dmatsgrp  22547  scmatsgrp  22567  scmatsgrp1  22570  m2cpmrngiso  22806  bastg  23014  tgss  23016  tgtop  23021  tgidm  23028  en2top  23033  neisspw  23155  topssnei  23172  neiptopuni  23178  lpss3  23192  clslp  23196  tgrest  23207  ssrest  23224  restntr  23230  ordtbas2  23239  ordtbas  23240  cnss1  23324  cnss2  23325  cnsscnp  23327  cnrest2r  23335  cmpsublem  23447  cmpsub  23448  tgcmp  23449  cmpcld  23450  hauscmplem  23454  cnconn  23470  llyss  23527  nllyss  23528  restnlly  23530  restlly  23531  locfincmp  23574  locfincf  23579  kgenss  23591  kgenidm  23595  llycmpkgen2  23598  1stckgen  23602  kgen2ss  23603  kgencn3  23606  ptbasfi  23629  ptpjopn  23660  txdis  23680  txkgen  23700  xkoptsub  23702  xkopjcn  23704  txconn  23737  qtoptop2  23747  qtopuni  23750  qtopkgen  23758  basqtop  23759  tgqtop  23760  qtopss  23763  qtoprest  23765  qtopomap  23766  qtopcmap  23767  kqsat  23779  kqcldsat  23781  hmphdis  23844  isfild  23906  ssfg  23920  fgss  23921  fgss2  23922  fgfil  23923  fgabs  23927  filconn  23931  fgtr  23938  uzrest  23945  ufilmax  23955  ufileu  23967  filufint  23968  rnelfm  24001  fmfnfmlem2  24003  fmfnfmlem4  24005  flimss2  24020  flimss1  24021  flimclsi  24026  flimcf  24030  flimsncls  24034  fclssscls  24066  fclsss1  24070  fclsss2  24071  fclscf  24073  uffclsflim  24079  alexsublem  24092  alexsubALTlem3  24097  ptcmplem2  24101  ptcmplem3  24102  cnextf  24114  efmndtmd  24149  symgtgp  24154  cldsubg  24159  tsmscl  24183  haustsms2  24185  tgptsmscls  24198  tsmsxp  24203  restutop  24285  ustuqtop4  24292  utop2nei  24298  utop3cls  24299  ucncn  24332  xblss2ps  24449  xblss2  24450  xrsblre  24860  xrsmopn  24861  recld2  24863  zdis  24865  icccmplem2  24872  cncfss  24949  cnheiborlem  25004  htpycn  25023  phtpyhtpy  25032  pi1blem  25089  cphsscph  25301  cfilfcls  25324  iscmet3lem2  25342  iscmet2  25344  caussi  25347  equivcfil  25349  lmcau  25363  metsscmetcld  25365  hlhil  25493  ivthicc  25508  ovoliunnul  25557  ovolicopnf  25574  uniioombllem3  25635  dyadmbllem  25649  volsup2  25655  vitalilem2  25659  itg1addlem4  25749  itg10a  25760  itg1ge0a  25761  mbfi1fseqlem4  25768  itg2gt0  25810  limciun  25944  perfdvf  25953  cpnord  25985  dvcj  26000  dvlip2  26045  dvivth  26060  dvne0  26061  dvcnvre  26069  ply1lpir  26230  plyco0  26240  plyexmo  26365  abelth  26492  efif1o  26599  logno1  26689  efopnlem2  26710  loglesqrt  26814  lgamcvg2  27107  ppisval  27156  ppinprm  27204  chtnprm  27206  fsumvma  27265  dchrfi  27307  chtppilimlem2  27526  chebbnd2  27529  vmadivsumb  27535  rplogsumlem2  27537  dchrisumlem2  27542  vmalogdivsum2  27590  vmalogdivsum  27591  2vmadivsumlem  27592  selbergb  27601  selberg2b  27604  selberg3lem1  27609  selberg3lem2  27610  selberg3  27611  selberg4lem1  27612  selberg4  27613  pntrlog2bndlem2  27630  pntrlog2bndlem4  27632  oldssmade  27948  ltslpss  27989  noseqrdgfn  28387  n0ssoldg  28434  peano5uzs  28485  uhgredgss  29289  usgruspgrb  29341  uhgrissubgr  29433  uhgrspansubgrlem  29448  uhgrspan1  29461  cusgredg  29582  usgredgsscusgredg  29617  ococss  31453  shsub1  31484  shless  31519  shmodsi  31549  pjhth  31553  spansnss  31731  spanpr  31740  spansnm0i  31810  pjjsi  31860  sumdmdii  32575  sumdmdlem  32578  sumdmdlem2  32579  cdj3lem1  32594  abrexss  32671  fnpreimac  32833  rnmposs  32836  uzssico  32947  ssnnssfz  32950  pwrssmgc  33139  pmtrcnel  33230  cycpmrn  33284  cyc3evpm  33291  cycpmgcl  33294  elrgspnlem1  33384  elrgspnlem3  33386  elrgspnlem4  33387  elrgspnsubrunlem2  33390  fldgensdrg  33462  ringlsmss1  33543  ringlsmss2  33544  prmidlssidl  33592  mxidlirredi  33620  drngmxidl  33626  drngmxidlr  33627  1arithidomlem1  33692  1arithidom  33694  1arithufdlem2  33702  1arithufdlem3  33703  1arithufdlem4  33704  dfufd2lem  33706  ply1mulrtss  33739  esplyfvaln  33832  dimkerim  33885  extdg1id  33924  irngss  33945  irngssv  33946  algextdeglem8  33982  constrsscn  33998  constrsslem  33999  constrsdrg  34033  crefss  34107  cmpcref  34108  zarmxt1  34138  tpr2rico  34170  esumrnmpt2  34326  esumpcvgval  34336  ldsysgenld  34418  sigapildsys  34420  ldgenpisys  34424  cldssbrsiga  34445  measdivcstALTV  34483  mbfmcnt  34526  oddpwdc  34612  eulerpartlemgs2  34638  reprpmtf1o  34881  bnj1033  35225  bnj1398  35290  trssfir1om  35368  r1omhfb  35369  trssfir1omregs  35393  r1omhfbregs  35394  sconnpi1  35550  cvmscld  35584  cvmliftlem15  35609  satfrnmapom  35681  dfon2lem6  36097  fnessref  36678  fgmin  36691  tailfb  36698  dissneqlem  37795  icoreresf  37807  rdglimss  37832  finxpreclem6  37851  lindsenlbs  38075  poimirlem11  38091  poimirlem12  38092  sstotbnd3  38236  prdstotbnd  38254  cntotbnd  38256  ismtyhmeo  38265  1idl  38486  disjdmqsss  39365  lshpdisj  39572  lssats  39597  lkrin  39749  glbconxN  39963  paddss1  40402  paddss2  40403  paddasslem16  40420  paddidm  40426  pmodlem2  40432  pmapjoin  40437  pmapjat1  40438  pclfinN  40485  pclfinclN  40535  diasslssN  41644  dia2dimlem12  41660  dihsslss  41861  baerlem3lem2  42295  baerlem5alem2  42296  baerlem5blem2  42297  zndvdchrrhm  42551  dvrelog2  42642  dvrelog3  42643  aks4d1p3  42656  aks4d1p4  42657  aks4d1p5  42658  aks4d1p7  42661  aks4d1p8  42665  primrootsunit1  42675  primrootscoprmpow  42677  primrootscoprbij  42680  hashscontpow1  42699  aks6d1c4  42702  sticksstones3  42726  aks6d1c6lem3  42750  aks6d1c6isolem2  42753  aks6d1c6lem5  42755  rhmqusspan  42763  unitscyglem1  42773  unitscyglem4  42776  eldiophss  43316  rencldnfilem  43358  pellexlem5  43371  pell14qrss1234  43394  pell1qrss14  43406  pellfundre  43419  pellfundge  43420  pellfundlb  43422  pellfundglb  43423  harinf  43572  proot1hash  43733  safesnsupfiss  43952  intabssd  44056  ss2iundf  44196  ov2ssiunov2  44237  clsk1indlem3  44580  radcnvrat  44851  nznngen  44853  trsspwALT3  45356  sspwimpALT2  45464  refsumcn  45571  iinssf  45677  icoiccdif  46061  icccncfext  46422  stoweidlem27  46562  stoweidlem46  46581  stoweidlem57  46592  fourierdlem40  46682  fourierdlem78  46719  ffnafv  47726  iccpartrn  47997  sprsymrelfvlem  48057  sprsymrelf1lem  48058  clnbgrssedg  48424  stgrusgra  48542  rhmsubcALTVlem4  48867  funcringcsetcALTV2lem8  48880  funcringcsetclem8ALTV  48903  ssnn0ssfz  48932  lincolss  49017  lcoss  49019  lcosslsp  49021  iunord  50258