Theorem ssrdv 3936

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ss 3915

This theorem is referenced by:  eqelssd  3952  ss2abdv  4014  sscon  4092  ssdif  4093  unss1  4134  ssrin  4191  eq0rdvALT  4357  sspw  4562  elpwdifsn  4742  uniss  4868  intss1  4915  intmin  4920  intssuni  4922  iinssiun  4957  iunss1  4958  iinss1  4959  ss2iun  4962  ssiun  4999  ssiun2  5000  iinss  5009  iinss2  5010  iunxdif3  5047  sspwb  5394  pwssun  5513  relop  5796  dmss  5848  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  imadifssran  6105  ssrnres  6132  sossfld  6140  predtrss  6276  preddowncl  6286  tron  6336  tz7.7  6339  funimassd  6896  dffv2  6925  chfnrn  6990  fvn0ssdmfun  7015  fveqdmss  7019  dff3  7041  ffnfv  7060  f1imass  7206  ssorduni  7720  onint  7731  limsssuc  7788  limuni3  7790  limomss  7809  fo1stres  7955  fo2ndres  7956  fo2ndf  8059  fnse  8071  ressuppssdif  8123  suppss  8132  reldmtpos  8172  fprlem2  8239  onfununi  8269  smoiun  8289  smocdmdom  8296  tz7.48-1  8370  tz7.49  8372  oaass  8484  cofon1  8595  cofon2  8596  qsss  8708  uniinqs  8729  pmss12g  8801  mapss  8821  ixpssmap2g  8859  ixpssmapg  8860  pssnn  9087  fineqv  9160  finnzfsuppd  9266  ssfii  9312  dffi2  9316  oismo  9435  unxpwdom2  9483  inf3lemd  9526  inf3lem1  9527  inf3lem6  9532  cantnflem3  9590  cantnf  9592  cnfcom3lem  9602  onssr1  9733  rankunb  9752  tcrank  9786  harcard  9880  carduni  9883  infxpenlem  9913  infpwfien  9962  dfac12r  10047  ackbij2lem1  10118  ackbij1lem18  10136  isfin1-3  10286  fin1a2lem11  10310  fin1a2lem13  10312  zorn2lem4  10399  zorn2lem5  10400  ttukeylem6  10414  ttukeylem7  10415  fpwwe2lem10  10540  fpwwe2lem11  10541  fpwwe2  10543  wunr1om  10619  wunom  10620  tskr1om  10667  tskr1om2  10668  tskxpss  10672  tskcard  10681  tskuni  10683  grothomex  10729  genpss  10904  distrlem1pr  10925  distrlem5pr  10927  ltexprlem2  10937  ltexprlem6  10941  ltexprlem7  10942  reclem3pr  10949  reclem4pr  10950  supaddc  12098  supadd  12099  supmul1  12100  supmullem2  12102  peano5uzi  12570  uzss  12763  ixxdisj  13264  ixxss1  13267  ixxss2  13268  ixxss12  13269  ixxub  13270  ixxlb  13271  iocssre  13331  icossre  13332  iccssre  13333  icodisj  13380  fzss1  13467  fzss2  13468  ssfzunsnext  13473  fzosplit  13596  fzouzsplit  13598  ssfzo12bi  13665  ssnn0fi  13896  fsuppmapnn0fiub  13902  suppssfz  13905  sswrd  14433  rtrclreclem3  14971  isercoll  15579  summolem2a  15626  fsumcvg3  15640  fsum2dlem  15681  fsumcom2  15685  qshash  15738  prodmolem2a  15845  fprod2dlem  15891  fprodcom2  15895  bitsfzo  16350  1arith  16843  vdwlem2  16898  vdwlem6  16902  vdwlem8  16904  ramtlecl  16916  prmgaplem3  16969  prmgaplem4  16970  monhom  17646  epihom  17653  funcsetcres2  18004  funcestrcsetclem8  18057  funcsetcestrclem8  18072  psdmrn  18483  chnrss  18525  chndss  18526  gsumwspan  18758  frmdss2  18775  sursubmefmnd  18808  injsubmefmnd  18809  trivsubgsnd  19070  ssnmz  19082  trivnsgd  19088  kerf1ghm  19163  conjnmz  19168  symgvalstruct  19313  gex1  19507  sylow2alem1  19533  lsmless1x  19560  lsmless2x  19561  lsmub1x  19562  lsmub2x  19563  lsmmod  19591  lsmdisj2  19598  efgrelexlemb  19666  efgcpbllemb  19671  cntzcmn  19756  gsum2d2  19890  dprdub  19943  dprdss  19947  dprddisj2  19957  pgpfac1lem3  19995  subrngmre  20481  subrguss  20506  subrgmre  20516  rnghmsscmap2  20548  rnghmsscmap  20549  funcrngcsetc  20559  funcrngcsetcALT  20560  rhmsscmap2  20577  rhmsscmap  20578  rhmsscrnghm  20584  rngcresringcat  20588  funcringcsetc  20593  unitrrg  20622  isdrng2  20662  primefld0cl  20725  primefld1cl  20726  lssssr  20891  lsssssubg  20895  lssmre  20903  lbspss  21020  lspdisj  21066  lbsextlem2  21100  lidl1el  21167  drngnidl  21184  lpiss  21270  zsssubrg  21366  qsssubdrg  21367  cnsubrg  21368  mulgrhm2  21419  znrrg  21506  ocvocv  21612  ocv2ss  21614  ocvin  21615  lsmcss  21633  cssmre  21634  pjcss  21657  lindfrn  21762  sraassab  21809  mhpsubg  22071  evls1maprnss  22296  dmatsgrp  22417  scmatsgrp  22437  scmatsgrp1  22440  m2cpmrngiso  22676  bastg  22884  tgss  22886  tgtop  22891  tgidm  22898  en2top  22903  neisspw  23025  topssnei  23042  neiptopuni  23048  lpss3  23062  clslp  23066  tgrest  23077  ssrest  23094  restntr  23100  ordtbas2  23109  ordtbas  23110  cnss1  23194  cnss2  23195  cnsscnp  23197  cnrest2r  23205  cmpsublem  23317  cmpsub  23318  tgcmp  23319  cmpcld  23320  hauscmplem  23324  cnconn  23340  llyss  23397  nllyss  23398  restnlly  23400  restlly  23401  locfincmp  23444  locfincf  23449  kgenss  23461  kgenidm  23465  llycmpkgen2  23468  1stckgen  23472  kgen2ss  23473  kgencn3  23476  ptbasfi  23499  ptpjopn  23530  txdis  23550  txkgen  23570  xkoptsub  23572  xkopjcn  23574  txconn  23607  qtoptop2  23617  qtopuni  23620  qtopkgen  23628  basqtop  23629  tgqtop  23630  qtopss  23633  qtoprest  23635  qtopomap  23636  qtopcmap  23637  kqsat  23649  kqcldsat  23651  hmphdis  23714  isfild  23776  ssfg  23790  fgss  23791  fgss2  23792  fgfil  23793  fgabs  23797  filconn  23801  fgtr  23808  uzrest  23815  ufilmax  23825  ufileu  23837  filufint  23838  rnelfm  23871  fmfnfmlem2  23873  fmfnfmlem4  23875  flimss2  23890  flimss1  23891  flimclsi  23896  flimcf  23900  flimsncls  23904  fclssscls  23936  fclsss1  23940  fclsss2  23941  fclscf  23943  uffclsflim  23949  alexsublem  23962  alexsubALTlem3  23967  ptcmplem2  23971  ptcmplem3  23972  cnextf  23984  efmndtmd  24019  symgtgp  24024  cldsubg  24029  tsmscl  24053  haustsms2  24055  tgptsmscls  24068  tsmsxp  24073  restutop  24155  ustuqtop4  24162  utop2nei  24168  utop3cls  24169  ucncn  24202  xblss2ps  24319  xblss2  24320  xrsblre  24730  xrsmopn  24731  recld2  24733  zdis  24735  icccmplem2  24742  cncfss  24822  cnheiborlem  24883  htpycn  24902  phtpyhtpy  24911  pi1blem  24969  cphsscph  25181  cfilfcls  25204  iscmet3lem2  25222  iscmet2  25224  caussi  25227  equivcfil  25229  lmcau  25243  metsscmetcld  25245  hlhil  25373  ivthicc  25389  ovoliunnul  25438  ovolicopnf  25455  uniioombllem3  25516  dyadmbllem  25530  volsup2  25536  vitalilem2  25540  itg1addlem4  25630  itg10a  25641  itg1ge0a  25642  mbfi1fseqlem4  25649  itg2gt0  25691  limciun  25825  perfdvf  25834  cpnord  25867  dvcj  25884  dvlip2  25930  dvivth  25945  dvne0  25946  dvcnvre  25954  ply1lpir  26117  plyco0  26127  plyexmo  26251  abelth  26381  efif1o  26485  logno1  26575  efopnlem2  26596  loglesqrt  26701  lgamcvg2  26995  ppisval  27044  ppinprm  27092  chtnprm  27094  fsumvma  27154  dchrfi  27196  chtppilimlem2  27415  chebbnd2  27418  vmadivsumb  27424  rplogsumlem2  27426  dchrisumlem2  27431  vmalogdivsum2  27479  vmalogdivsum  27480  2vmadivsumlem  27481  selbergb  27490  selberg2b  27493  selberg3lem1  27498  selberg3lem2  27499  selberg3  27500  selberg4lem1  27501  selberg4  27502  pntrlog2bndlem2  27519  pntrlog2bndlem4  27521  oldssmade  27825  sltlpss  27856  noseqrdgfn  28239  peano5uzs  28331  uhgredgss  29113  usgruspgrb  29165  uhgrissubgr  29257  uhgrspansubgrlem  29272  uhgrspan1  29285  cusgredg  29406  usgredgsscusgredg  29442  ococss  31277  shsub1  31308  shless  31343  shmodsi  31373  pjhth  31377  spansnss  31555  spanpr  31564  spansnm0i  31634  pjjsi  31684  sumdmdii  32399  sumdmdlem  32402  sumdmdlem2  32403  cdj3lem1  32418  abrexss  32496  fnpreimac  32657  rnmposs  32660  unifi3  32700  uzssico  32773  ssnnssfz  32776  pwrssmgc  32990  pmtrcnel  33067  cycpmrn  33121  cyc3evpm  33128  cycpmgcl  33131  elrgspnlem1  33218  elrgspnlem3  33220  elrgspnlem4  33221  elrgspnsubrunlem2  33224  fldgensdrg  33289  ringlsmss1  33370  ringlsmss2  33371  prmidlssidl  33419  mxidlirredi  33445  drngmxidl  33451  drngmxidlr  33452  1arithidomlem1  33509  1arithidom  33511  1arithufdlem2  33519  1arithufdlem3  33520  1arithufdlem4  33521  dfufd2lem  33523  ply1mulrtss  33554  dimkerim  33663  extdg1id  33702  irngss  33723  irngssv  33724  algextdeglem8  33760  constrsscn  33776  constrsslem  33777  constrsdrg  33811  crefss  33885  cmpcref  33886  zarmxt1  33916  tpr2rico  33948  esumrnmpt2  34104  esumpcvgval  34114  ldsysgenld  34196  sigapildsys  34198  ldgenpisys  34202  cldssbrsiga  34223  measdivcstALTV  34261  mbfmcnt  34304  oddpwdc  34390  eulerpartlemgs2  34416  reprpmtf1o  34662  bnj1033  35004  bnj1398  35069  trssfir1om  35145  r1omhfb  35146  trssfir1omregs  35155  r1omhfbregs  35156  sconnpi1  35306  cvmscld  35340  cvmliftlem15  35365  satfrnmapom  35437  dfon2lem6  35853  fnessref  36424  fgmin  36437  tailfb  36444  dissneqlem  37407  icoreresf  37419  rdglimss  37444  finxpreclem6  37463  lindsenlbs  37678  poimirlem11  37694  poimirlem12  37695  sstotbnd3  37839  prdstotbnd  37857  cntotbnd  37859  ismtyhmeo  37868  1idl  38089  disjdmqsss  38923  lshpdisj  39109  lssats  39134  lkrin  39286  glbconxN  39500  paddss1  39939  paddss2  39940  paddasslem16  39957  paddidm  39963  pmodlem2  39969  pmapjoin  39974  pmapjat1  39975  pclfinN  40022  pclfinclN  40072  diasslssN  41181  dia2dimlem12  41197  dihsslss  41398  baerlem3lem2  41832  baerlem5alem2  41833  baerlem5blem2  41834  zndvdchrrhm  42088  dvrelog2  42180  dvrelog3  42181  aks4d1p3  42194  aks4d1p4  42195  aks4d1p5  42196  aks4d1p7  42199  aks4d1p8  42203  primrootsunit1  42213  primrootscoprmpow  42215  primrootscoprbij  42218  hashscontpow1  42237  aks6d1c4  42240  sticksstones3  42264  aks6d1c6lem3  42288  aks6d1c6isolem2  42291  aks6d1c6lem5  42293  rhmqusspan  42301  unitscyglem1  42311  unitscyglem4  42314  ss2ab1  42340  eldiophss  42894  rencldnfilem  42940  pellexlem5  42953  pell14qrss1234  42976  pell1qrss14  42988  pellfundre  43001  pellfundge  43002  pellfundlb  43004  pellfundglb  43005  harinf  43154  proot1hash  43315  safesnsupfiss  43535  intabssd  43639  ss2iundf  43779  ov2ssiunov2  43820  clsk1indlem3  44163  radcnvrat  44434  nznngen  44436  trsspwALT3  44939  sspwimpALT2  45047  refsumcn  45154  iinssf  45262  icoiccdif  45651  icccncfext  46012  stoweidlem27  46152  stoweidlem46  46171  stoweidlem57  46182  fourierdlem40  46272  fourierdlem78  46309  ffnafv  47298  iccpartrn  47557  sprsymrelfvlem  47617  sprsymrelf1lem  47618  clnbgrssedg  47968  stgrusgra  48086  rhmsubcALTVlem4  48411  funcringcsetcALTV2lem8  48424  funcringcsetclem8ALTV  48447  ssnn0ssfz  48476  lincolss  48562  lcoss  48564  lcosslsp  48566  iunord  49804