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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111   ⊆ wss 3902

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 3919

This theorem is referenced by:  eqelssd  3956  ss2abdv  4017  sscon  4093  ssdif  4094  unss1  4135  ssrin  4192  eq0rdvALT  4358  sspw  4561  elpwdifsn  4741  uniss  4867  intss1  4913  intmin  4918  intssuni  4920  iinssiun  4955  iunss1  4956  iinss1  4957  ss2iun  4960  ssiun  4995  ssiun2  4996  iinss  5005  iinss2  5006  iunxdif3  5043  sspwb  5390  pwssun  5508  relop  5790  dmss  5842  dmcosseq  5917  dmcosseqOLD  5918  dmcosseqOLDOLD  5919  imadifssran  6098  ssrnres  6125  sossfld  6133  predtrss  6269  preddowncl  6279  tron  6329  tz7.7  6332  funimassd  6888  dffv2  6917  chfnrn  6982  fvn0ssdmfun  7007  fveqdmss  7011  dff3  7033  ffnfv  7052  f1imass  7198  ssorduni  7712  onint  7723  limsssuc  7780  limuni3  7782  limomss  7801  fo1stres  7947  fo2ndres  7948  fo2ndf  8051  fnse  8063  ressuppssdif  8115  suppss  8124  reldmtpos  8164  fprlem2  8231  onfununi  8261  smoiun  8281  smocdmdom  8288  tz7.48-1  8362  tz7.49  8364  oaass  8476  cofon1  8587  cofon2  8588  qsss  8700  uniinqs  8721  pmss12g  8793  mapss  8813  ixpssmap2g  8851  ixpssmapg  8852  pssnn  9078  fineqv  9151  finnzfsuppd  9257  ssfii  9303  dffi2  9307  oismo  9426  unxpwdom2  9474  inf3lemd  9517  inf3lem1  9518  inf3lem6  9523  cantnflem3  9581  cantnf  9583  cnfcom3lem  9593  onssr1  9724  rankunb  9743  tcrank  9777  harcard  9871  carduni  9874  infxpenlem  9904  infpwfien  9953  dfac12r  10038  ackbij2lem1  10109  ackbij1lem18  10127  isfin1-3  10277  fin1a2lem11  10301  fin1a2lem13  10303  zorn2lem4  10390  zorn2lem5  10391  ttukeylem6  10405  ttukeylem7  10406  fpwwe2lem10  10531  fpwwe2lem11  10532  fpwwe2  10534  wunr1om  10610  wunom  10611  tskr1om  10658  tskr1om2  10659  tskxpss  10663  tskcard  10672  tskuni  10674  grothomex  10720  genpss  10895  distrlem1pr  10916  distrlem5pr  10918  ltexprlem2  10928  ltexprlem6  10932  ltexprlem7  10933  reclem3pr  10940  reclem4pr  10941  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  peano5uzi  12562  uzss  12755  ixxdisj  13260  ixxss1  13263  ixxss2  13264  ixxss12  13265  ixxub  13266  ixxlb  13267  iocssre  13327  icossre  13328  iccssre  13329  icodisj  13376  fzss1  13463  fzss2  13464  ssfzunsnext  13469  fzosplit  13592  fzouzsplit  13594  ssfzo12bi  13661  ssnn0fi  13892  fsuppmapnn0fiub  13898  suppssfz  13901  sswrd  14429  rtrclreclem3  14967  isercoll  15575  summolem2a  15622  fsumcvg3  15636  fsum2dlem  15677  fsumcom2  15681  qshash  15734  prodmolem2a  15841  fprod2dlem  15887  fprodcom2  15891  bitsfzo  16346  1arith  16839  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  ramtlecl  16912  prmgaplem3  16965  prmgaplem4  16966  monhom  17642  epihom  17649  funcsetcres2  18000  funcestrcsetclem8  18053  funcsetcestrclem8  18068  psdmrn  18479  chnrss  18521  chndss  18522  gsumwspan  18754  frmdss2  18771  sursubmefmnd  18804  injsubmefmnd  18805  trivsubgsnd  19067  ssnmz  19079  trivnsgd  19085  kerf1ghm  19160  conjnmz  19165  symgvalstruct  19310  gex1  19504  sylow2alem1  19530  lsmless1x  19557  lsmless2x  19558  lsmub1x  19559  lsmub2x  19560  lsmmod  19588  lsmdisj2  19595  efgrelexlemb  19663  efgcpbllemb  19668  cntzcmn  19753  gsum2d2  19887  dprdub  19940  dprdss  19944  dprddisj2  19954  pgpfac1lem3  19992  subrngmre  20478  subrguss  20503  subrgmre  20513  rnghmsscmap2  20545  rnghmsscmap  20546  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  rngcresringcat  20585  funcringcsetc  20590  unitrrg  20619  isdrng2  20659  primefld0cl  20722  primefld1cl  20723  lssssr  20888  lsssssubg  20892  lssmre  20900  lbspss  21017  lspdisj  21063  lbsextlem2  21097  lidl1el  21164  drngnidl  21181  lpiss  21267  zsssubrg  21363  qsssubdrg  21364  cnsubrg  21365  mulgrhm2  21416  znrrg  21503  ocvocv  21609  ocv2ss  21611  ocvin  21612  lsmcss  21630  cssmre  21631  pjcss  21654  lindfrn  21759  sraassab  21806  mhpsubg  22069  evls1maprnss  22294  dmatsgrp  22415  scmatsgrp  22435  scmatsgrp1  22438  m2cpmrngiso  22674  bastg  22882  tgss  22884  tgtop  22889  tgidm  22896  en2top  22901  neisspw  23023  topssnei  23040  neiptopuni  23046  lpss3  23060  clslp  23064  tgrest  23075  ssrest  23092  restntr  23098  ordtbas2  23107  ordtbas  23108  cnss1  23192  cnss2  23193  cnsscnp  23195  cnrest2r  23203  cmpsublem  23315  cmpsub  23316  tgcmp  23317  cmpcld  23318  hauscmplem  23322  cnconn  23338  llyss  23395  nllyss  23396  restnlly  23398  restlly  23399  locfincmp  23442  locfincf  23447  kgenss  23459  kgenidm  23463  llycmpkgen2  23466  1stckgen  23470  kgen2ss  23471  kgencn3  23474  ptbasfi  23497  ptpjopn  23528  txdis  23548  txkgen  23568  xkoptsub  23570  xkopjcn  23572  txconn  23605  qtoptop2  23615  qtopuni  23618  qtopkgen  23626  basqtop  23627  tgqtop  23628  qtopss  23631  qtoprest  23633  qtopomap  23634  qtopcmap  23635  kqsat  23647  kqcldsat  23649  hmphdis  23712  isfild  23774  ssfg  23788  fgss  23789  fgss2  23790  fgfil  23791  fgabs  23795  filconn  23799  fgtr  23806  uzrest  23813  ufilmax  23823  ufileu  23835  filufint  23836  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  flimss2  23888  flimss1  23889  flimclsi  23894  flimcf  23898  flimsncls  23902  fclssscls  23934  fclsss1  23938  fclsss2  23939  fclscf  23941  uffclsflim  23947  alexsublem  23960  alexsubALTlem3  23965  ptcmplem2  23969  ptcmplem3  23970  cnextf  23982  efmndtmd  24017  symgtgp  24022  cldsubg  24027  tsmscl  24051  haustsms2  24053  tgptsmscls  24066  tsmsxp  24071  restutop  24153  ustuqtop4  24160  utop2nei  24166  utop3cls  24167  ucncn  24200  xblss2ps  24317  xblss2  24318  xrsblre  24728  xrsmopn  24729  recld2  24731  zdis  24733  icccmplem2  24740  cncfss  24820  cnheiborlem  24881  htpycn  24900  phtpyhtpy  24909  pi1blem  24967  cphsscph  25179  cfilfcls  25202  iscmet3lem2  25220  iscmet2  25222  caussi  25225  equivcfil  25227  lmcau  25241  metsscmetcld  25243  hlhil  25371  ivthicc  25387  ovoliunnul  25436  ovolicopnf  25453  uniioombllem3  25514  dyadmbllem  25528  volsup2  25534  vitalilem2  25538  itg1addlem4  25628  itg10a  25639  itg1ge0a  25640  mbfi1fseqlem4  25647  itg2gt0  25689  limciun  25823  perfdvf  25832  cpnord  25865  dvcj  25882  dvlip2  25928  dvivth  25943  dvne0  25944  dvcnvre  25952  ply1lpir  26115  plyco0  26125  plyexmo  26249  abelth  26379  efif1o  26483  logno1  26573  efopnlem2  26594  loglesqrt  26699  lgamcvg2  26993  ppisval  27042  ppinprm  27090  chtnprm  27092  fsumvma  27152  dchrfi  27194  chtppilimlem2  27413  chebbnd2  27416  vmadivsumb  27422  rplogsumlem2  27424  dchrisumlem2  27429  vmalogdivsum2  27477  vmalogdivsum  27478  2vmadivsumlem  27479  selbergb  27488  selberg2b  27491  selberg3lem1  27496  selberg3lem2  27497  selberg3  27498  selberg4lem1  27499  selberg4  27500  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  oldssmade  27823  sltlpss  27854  noseqrdgfn  28237  peano5uzs  28329  uhgredgss  29110  usgruspgrb  29162  uhgrissubgr  29254  uhgrspansubgrlem  29269  uhgrspan1  29282  cusgredg  29403  usgredgsscusgredg  29439  ococss  31271  shsub1  31302  shless  31337  shmodsi  31367  pjhth  31371  spansnss  31549  spanpr  31558  spansnm0i  31628  pjjsi  31678  sumdmdii  32393  sumdmdlem  32396  sumdmdlem2  32397  cdj3lem1  32412  abrexss  32490  fnpreimac  32651  rnmposs  32654  unifi3  32692  uzssico  32765  ssnnssfz  32768  pwrssmgc  32979  pmtrcnel  33056  cycpmrn  33110  cyc3evpm  33117  cycpmgcl  33120  elrgspnlem1  33207  elrgspnlem3  33209  elrgspnlem4  33210  elrgspnsubrunlem2  33213  fldgensdrg  33278  ringlsmss1  33359  ringlsmss2  33360  prmidlssidl  33408  mxidlirredi  33434  drngmxidl  33440  drngmxidlr  33441  1arithidomlem1  33498  1arithidom  33500  1arithufdlem2  33508  1arithufdlem3  33509  1arithufdlem4  33510  dfufd2lem  33512  ply1mulrtss  33543  dimkerim  33638  extdg1id  33677  irngss  33698  irngssv  33699  algextdeglem8  33735  constrsscn  33751  constrsslem  33752  constrsdrg  33786  crefss  33860  cmpcref  33861  zarmxt1  33891  tpr2rico  33923  esumrnmpt2  34079  esumpcvgval  34089  ldsysgenld  34171  sigapildsys  34173  ldgenpisys  34177  cldssbrsiga  34198  measdivcstALTV  34236  mbfmcnt  34279  oddpwdc  34365  eulerpartlemgs2  34391  reprpmtf1o  34637  bnj1033  34979  bnj1398  35044  trssfir1om  35120  r1omhfb  35121  trssfir1omregs  35130  r1omhfbregs  35131  sconnpi1  35281  cvmscld  35315  cvmliftlem15  35340  satfrnmapom  35412  dfon2lem6  35828  fnessref  36397  fgmin  36410  tailfb  36417  dissneqlem  37380  icoreresf  37392  rdglimss  37417  finxpreclem6  37436  lindsenlbs  37661  poimirlem11  37677  poimirlem12  37678  sstotbnd3  37822  prdstotbnd  37840  cntotbnd  37842  ismtyhmeo  37851  1idl  38072  disjdmqsss  38846  lshpdisj  39032  lssats  39057  lkrin  39209  glbconxN  39423  paddss1  39862  paddss2  39863  paddasslem16  39880  paddidm  39886  pmodlem2  39892  pmapjoin  39897  pmapjat1  39898  pclfinN  39945  pclfinclN  39995  diasslssN  41104  dia2dimlem12  41120  dihsslss  41321  baerlem3lem2  41755  baerlem5alem2  41756  baerlem5blem2  41757  zndvdchrrhm  42011  dvrelog2  42103  dvrelog3  42104  aks4d1p3  42117  aks4d1p4  42118  aks4d1p5  42119  aks4d1p7  42122  aks4d1p8  42126  primrootsunit1  42136  primrootscoprmpow  42138  primrootscoprbij  42141  hashscontpow1  42160  aks6d1c4  42163  sticksstones3  42187  aks6d1c6lem3  42211  aks6d1c6isolem2  42214  aks6d1c6lem5  42216  rhmqusspan  42224  unitscyglem1  42234  unitscyglem4  42237  ss2ab1  42258  eldiophss  42813  rencldnfilem  42859  pellexlem5  42872  pell14qrss1234  42895  pell1qrss14  42907  pellfundre  42920  pellfundge  42921  pellfundlb  42923  pellfundglb  42924  harinf  43073  proot1hash  43234  safesnsupfiss  43454  intabssd  43558  ss2iundf  43698  ov2ssiunov2  43739  clsk1indlem3  44082  radcnvrat  44353  nznngen  44355  trsspwALT3  44858  sspwimpALT2  44966  refsumcn  45073  iinssf  45181  icoiccdif  45570  icccncfext  45931  stoweidlem27  46071  stoweidlem46  46090  stoweidlem57  46101  fourierdlem40  46191  fourierdlem78  46228  ffnafv  47208  iccpartrn  47467  sprsymrelfvlem  47527  sprsymrelf1lem  47528  clnbgrssedg  47878  stgrusgra  47996  rhmsubcALTVlem4  48321  funcringcsetcALTV2lem8  48334  funcringcsetclem8ALTV  48357  ssnn0ssfz  48386  lincolss  48472  lcoss  48474  lcosslsp  48476  iunord  49714