Theorem ssrdv 3923

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqelssd  3938  ss2abdvALT  3994  sscon  4069  ssdif  4070  unss1  4109  ssrin  4164  eq0rdvALT  4336  sspw  4543  elpwdifsn  4719  uniss  4844  intss1  4891  intmin  4896  intssuni  4898  iinssiun  4934  iunss1  4935  iinss1  4936  ss2iun  4939  ssiun  4972  ssiun2  4973  iinss  4982  iinss2  4983  iunxdif3  5020  sspwb  5359  pwssun  5476  relop  5748  dmss  5800  dmcosseq  5871  ssrnres  6070  sossfld  6078  predtrss  6214  preddowncl  6224  tron  6274  tz7.7  6277  dffv2  6845  chfnrn  6908  fvn0ssdmfun  6934  fveqdmss  6938  dff3  6958  ffnfv  6974  f1imass  7118  ssorduni  7606  onint  7617  limsssuc  7672  limuni3  7674  limomss  7692  fo1stres  7830  fo2ndres  7831  fo2ndf  7933  fnse  7945  ressuppssdif  7972  suppss  7981  suppssOLD  7982  reldmtpos  8021  fprlem2  8088  onfununi  8143  smoiun  8163  smorndom  8170  tz7.48-1  8244  tz7.49  8246  oaass  8354  qsss  8525  uniinqs  8544  pmss12g  8615  mapss  8635  ixpssmap2g  8673  ixpssmapg  8674  pssnn  8913  fineqv  8967  pssnnOLD  8969  ssfii  9108  dffi2  9112  oismo  9229  unxpwdom2  9277  inf3lemd  9315  inf3lem1  9316  inf3lem6  9321  cantnflem3  9379  cantnf  9381  cnfcom3lem  9391  onssr1  9520  rankunb  9539  tcrank  9573  harcard  9667  carduni  9670  infxpenlem  9700  infpwfien  9749  dfac12r  9833  ackbij2lem1  9906  ackbij1lem18  9924  isfin1-3  10073  fin1a2lem11  10097  fin1a2lem13  10099  zorn2lem4  10186  zorn2lem5  10187  ttukeylem6  10201  ttukeylem7  10202  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2  10330  wunr1om  10406  wunom  10407  tskr1om  10454  tskr1om2  10455  tskxpss  10459  tskcard  10468  tskuni  10470  grothomex  10516  genpss  10691  distrlem1pr  10712  distrlem5pr  10714  ltexprlem2  10724  ltexprlem6  10728  ltexprlem7  10729  reclem3pr  10736  reclem4pr  10737  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  peano5uzi  12339  uzss  12534  ixxdisj  13023  ixxss1  13026  ixxss2  13027  ixxss12  13028  ixxub  13029  ixxlb  13030  iocssre  13088  icossre  13089  iccssre  13090  icodisj  13137  fzss1  13224  fzss2  13225  ssfzunsnext  13230  fzosplit  13348  fzouzsplit  13350  ssfzo12bi  13410  ssnn0fi  13633  fsuppmapnn0fiub  13639  suppssfz  13642  sswrd  14153  rtrclreclem3  14699  isercoll  15307  summolem2a  15355  fsumcvg3  15369  fsum2dlem  15410  fsumcom2  15414  qshash  15467  prodmolem2a  15572  fprod2dlem  15618  fprodcom2  15622  bitsfzo  16070  1arith  16556  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  ramtlecl  16629  prmgaplem3  16682  prmgaplem4  16683  monhom  17364  epihom  17371  funcsetcres2  17724  funcestrcsetclem8  17780  funcsetcestrclem8  17795  psdmrn  18206  gsumwspan  18400  frmdss2  18417  sursubmefmnd  18450  injsubmefmnd  18451  trivsubgsnd  18697  ssnmz  18709  trivnsgd  18715  conjnmz  18783  symgvalstruct  18919  symgvalstructOLD  18920  gex1  19111  sylow2alem1  19137  lsmless1x  19164  lsmless2x  19165  lsmub1x  19166  lsmub2x  19167  lsmmod  19196  lsmdisj2  19203  efgrelexlemb  19271  efgcpbllemb  19276  cntzcmn  19356  gsum2d2  19490  dprdub  19543  dprdss  19547  dprddisj2  19557  pgpfac1lem3  19595  kerf1ghm  19902  isdrng2  19916  subrguss  19954  subrgmre  19963  primefld0cl  19989  primefld1cl  19990  lssssr  20130  lsssssubg  20135  lssmre  20143  lbspss  20259  lspdisj  20302  lbsextlem2  20336  lidl1el  20402  drngnidl  20413  lpiss  20434  unitrrg  20477  zsssubrg  20568  qsssubdrg  20569  cnsubrg  20570  mulgrhm2  20612  znrrg  20685  ocvocv  20788  ocv2ss  20790  ocvin  20791  lsmcss  20809  cssmre  20810  pjcss  20833  lindfrn  20938  mhpsubg  21253  dmatsgrp  21556  scmatsgrp  21576  scmatsgrp1  21579  m2cpmrngiso  21815  bastg  22024  tgss  22026  tgtop  22031  tgidm  22038  en2top  22043  neisspw  22166  topssnei  22183  neiptopuni  22189  lpss3  22203  clslp  22207  tgrest  22218  ssrest  22235  restntr  22241  ordtbas2  22250  ordtbas  22251  cnss1  22335  cnss2  22336  cnsscnp  22338  cnrest2r  22346  cmpsublem  22458  cmpsub  22459  tgcmp  22460  cmpcld  22461  hauscmplem  22465  cnconn  22481  llyss  22538  nllyss  22539  restnlly  22541  restlly  22542  locfincmp  22585  locfincf  22590  kgenss  22602  kgenidm  22606  llycmpkgen2  22609  1stckgen  22613  kgen2ss  22614  kgencn3  22617  ptbasfi  22640  ptpjopn  22671  txdis  22691  txkgen  22711  xkoptsub  22713  xkopjcn  22715  txconn  22748  qtoptop2  22758  qtopuni  22761  qtopkgen  22769  basqtop  22770  tgqtop  22771  qtopss  22774  qtoprest  22776  qtopomap  22777  qtopcmap  22778  kqsat  22790  kqcldsat  22792  hmphdis  22855  isfild  22917  ssfg  22931  fgss  22932  fgss2  22933  fgfil  22934  fgabs  22938  filconn  22942  fgtr  22949  uzrest  22956  ufilmax  22966  ufileu  22978  filufint  22979  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  flimss2  23031  flimss1  23032  flimclsi  23037  flimcf  23041  flimsncls  23045  fclssscls  23077  fclsss1  23081  fclsss2  23082  fclscf  23084  uffclsflim  23090  alexsublem  23103  alexsubALTlem3  23108  ptcmplem2  23112  ptcmplem3  23113  cnextf  23125  efmndtmd  23160  symgtgp  23165  cldsubg  23170  tsmscl  23194  haustsms2  23196  tgptsmscls  23209  tsmsxp  23214  restutop  23297  ustuqtop4  23304  utop2nei  23310  utop3cls  23311  ucncn  23345  xblss2ps  23462  xblss2  23463  xrsblre  23880  xrsmopn  23881  recld2  23883  zdis  23885  icccmplem2  23892  cncfss  23968  cnheiborlem  24023  htpycn  24042  phtpyhtpy  24051  pi1blem  24108  cphsscph  24320  cfilfcls  24343  iscmet3lem2  24361  iscmet2  24363  caussi  24366  equivcfil  24368  lmcau  24382  metsscmetcld  24384  hlhil  24512  ivthicc  24527  ovoliunnul  24576  ovolicopnf  24593  uniioombllem3  24654  dyadmbllem  24668  volsup2  24674  vitalilem2  24678  itg1addlem4  24768  itg1addlem4OLD  24769  itg10a  24780  itg1ge0a  24781  mbfi1fseqlem4  24788  itg2gt0  24830  limciun  24963  perfdvf  24972  cpnord  25004  dvcj  25019  dvlip2  25064  dvivth  25079  dvne0  25080  dvcnvre  25088  ply1lpir  25248  plyco0  25258  plyexmo  25378  abelth  25505  efif1o  25607  logno1  25696  efopnlem2  25717  loglesqrt  25816  lgamcvg2  26109  ppisval  26158  ppinprm  26206  chtnprm  26208  fsumvma  26266  dchrfi  26308  chtppilimlem2  26527  chebbnd2  26530  vmadivsumb  26536  rplogsumlem2  26538  dchrisumlem2  26543  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  selbergb  26602  selberg2b  26605  selberg3lem1  26610  selberg3lem2  26611  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  uhgredgss  27404  usgruspgrb  27454  uhgrissubgr  27545  uhgrspansubgrlem  27560  uhgrspan1  27573  cusgredg  27694  usgredgsscusgredg  27729  ococss  29556  shsub1  29587  shless  29622  shmodsi  29652  pjhth  29656  spansnss  29834  spanpr  29843  spansnm0i  29913  pjjsi  29963  sumdmdii  30678  sumdmdlem  30681  sumdmdlem2  30682  cdj3lem1  30697  abrexss  30758  fnpreimac  30910  rnmposs  30913  unifi3  30949  uzssico  31007  ssnnssfz  31010  pwrssmgc  31180  pmtrcnel  31260  cycpmrn  31312  cyc3evpm  31319  cycpmgcl  31322  ringlsmss1  31486  ringlsmss2  31487  prmidlssidl  31522  dimkerim  31610  extdg1id  31640  crefss  31701  cmpcref  31702  zarmxt1  31732  tpr2rico  31764  esumrnmpt2  31936  esumpcvgval  31946  ldsysgenld  32028  sigapildsys  32030  ldgenpisys  32034  cldssbrsiga  32055  measdivcstALTV  32093  mbfmcnt  32135  oddpwdc  32221  eulerpartlemgs2  32247  reprpmtf1o  32506  bnj1033  32849  bnj1398  32914  sconnpi1  33101  cvmscld  33135  cvmliftlem15  33160  satfrnmapom  33232  dfon2lem6  33670  oldssmade  33987  sltlpss  34014  fnessref  34473  fgmin  34486  tailfb  34493  dissneqlem  35438  icoreresf  35450  rdglimss  35475  finxpreclem6  35494  lindsenlbs  35699  poimirlem11  35715  poimirlem12  35716  sstotbnd3  35861  prdstotbnd  35879  cntotbnd  35881  ismtyhmeo  35890  1idl  36111  lshpdisj  36928  lssats  36953  lkrin  37105  glbconxN  37319  paddss1  37758  paddss2  37759  paddasslem16  37776  paddidm  37782  pmodlem2  37788  pmapjoin  37793  pmapjat1  37794  pclfinN  37841  pclfinclN  37891  diasslssN  39000  dia2dimlem12  39016  dihsslss  39217  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  dvrelog2  40000  dvrelog3  40001  aks4d1p3  40014  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8  40023  sticksstones3  40032  eldiophss  40512  rencldnfilem  40558  pellexlem5  40571  pell14qrss1234  40594  pell1qrss14  40606  pellfundre  40619  pellfundge  40620  pellfundlb  40622  pellfundglb  40623  harinf  40772  proot1hash  40941  intabssd  41024  ss2iundf  41156  ov2ssiunov2  41197  clsk1indlem3  41542  finnzfsuppd  41709  radcnvrat  41821  nznngen  41823  trsspwALT3  42329  sspwimpALT2  42437  refsumcn  42462  iinssf  42576  icoiccdif  42952  icccncfext  43318  stoweidlem27  43458  stoweidlem46  43477  stoweidlem57  43488  fourierdlem40  43578  fourierdlem78  43615  ffnafv  44550  iccpartrn  44770  sprsymrelfvlem  44830  sprsymrelf1lem  44831  rnghmsscmap2  45419  rnghmsscmap  45420  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap2  45465  rhmsscmap  45466  rhmsscrnghm  45472  rngcresringcat  45476  funcringcsetc  45481  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  rhmsubcALTVlem4  45553  ssnn0ssfz  45573  lincolss  45663  lcoss  45665  lcosslsp  45667  iunord  46268