Theorem ssrdv 4014

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  eqelssd  4030  ss2abdv  4089  sscon  4166  ssdif  4167  unss1  4208  ssrin  4263  eq0rdvALT  4431  sspw  4633  elpwdifsn  4814  uniss  4939  intss1  4987  intmin  4992  intssuni  4994  iinssiun  5028  iunss1  5029  iinss1  5030  ss2iun  5033  ssiun  5069  ssiun2  5070  iinss  5079  iinss2  5080  iunxdif3  5118  sspwb  5469  pwssun  5590  relop  5875  dmss  5927  dmcosseq  5999  dmcosseqOLD  6000  ssrnres  6209  sossfld  6217  predtrss  6354  preddowncl  6364  tron  6418  tz7.7  6421  funimassd  6988  dffv2  7017  chfnrn  7082  fvn0ssdmfun  7108  fveqdmss  7112  dff3  7134  ffnfv  7153  f1imass  7301  ssorduni  7814  onint  7826  limsssuc  7887  limuni3  7889  limomss  7908  fo1stres  8056  fo2ndres  8057  fo2ndf  8162  fnse  8174  ressuppssdif  8226  suppss  8235  reldmtpos  8275  fprlem2  8342  onfununi  8397  smoiun  8417  smocdmdom  8424  tz7.48-1  8499  tz7.49  8501  oaass  8617  cofon1  8728  cofon2  8729  qsss  8836  uniinqs  8855  pmss12g  8927  mapss  8947  ixpssmap2g  8985  ixpssmapg  8986  pssnn  9234  fineqv  9326  ssfii  9488  dffi2  9492  oismo  9609  unxpwdom2  9657  inf3lemd  9696  inf3lem1  9697  inf3lem6  9702  cantnflem3  9760  cantnf  9762  cnfcom3lem  9772  onssr1  9900  rankunb  9919  tcrank  9953  harcard  10047  carduni  10050  infxpenlem  10082  infpwfien  10131  dfac12r  10216  ackbij2lem1  10287  ackbij1lem18  10305  isfin1-3  10455  fin1a2lem11  10479  fin1a2lem13  10481  zorn2lem4  10568  zorn2lem5  10569  ttukeylem6  10583  ttukeylem7  10584  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2  10712  wunr1om  10788  wunom  10789  tskr1om  10836  tskr1om2  10837  tskxpss  10841  tskcard  10850  tskuni  10852  grothomex  10898  genpss  11073  distrlem1pr  11094  distrlem5pr  11096  ltexprlem2  11106  ltexprlem6  11110  ltexprlem7  11111  reclem3pr  11118  reclem4pr  11119  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  peano5uzi  12732  uzss  12926  ixxdisj  13422  ixxss1  13425  ixxss2  13426  ixxss12  13427  ixxub  13428  ixxlb  13429  iocssre  13487  icossre  13488  iccssre  13489  icodisj  13536  fzss1  13623  fzss2  13624  ssfzunsnext  13629  fzosplit  13749  fzouzsplit  13751  ssfzo12bi  13811  ssnn0fi  14036  fsuppmapnn0fiub  14042  suppssfz  14045  sswrd  14570  rtrclreclem3  15109  isercoll  15716  summolem2a  15763  fsumcvg3  15777  fsum2dlem  15818  fsumcom2  15822  qshash  15875  prodmolem2a  15982  fprod2dlem  16028  fprodcom2  16032  bitsfzo  16481  1arith  16974  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  ramtlecl  17047  prmgaplem3  17100  prmgaplem4  17101  monhom  17796  epihom  17803  funcsetcres2  18160  funcestrcsetclem8  18216  funcsetcestrclem8  18231  psdmrn  18643  gsumwspan  18881  frmdss2  18898  sursubmefmnd  18931  injsubmefmnd  18932  trivsubgsnd  19194  ssnmz  19206  trivnsgd  19212  kerf1ghm  19287  conjnmz  19292  symgvalstruct  19438  symgvalstructOLD  19439  gex1  19633  sylow2alem1  19659  lsmless1x  19686  lsmless2x  19687  lsmub1x  19688  lsmub2x  19689  lsmmod  19717  lsmdisj2  19724  efgrelexlemb  19792  efgcpbllemb  19797  cntzcmn  19882  gsum2d2  20016  dprdub  20069  dprdss  20073  dprddisj2  20083  pgpfac1lem3  20121  subrngmre  20588  subrguss  20615  subrgmre  20625  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap2  20680  rhmsscmap  20681  rhmsscrnghm  20687  rngcresringcat  20691  funcringcsetc  20696  unitrrg  20725  isdrng2  20765  primefld0cl  20829  primefld1cl  20830  lssssr  20975  lsssssubg  20979  lssmre  20987  lbspss  21104  lspdisj  21150  lbsextlem2  21184  lidl1el  21259  drngnidl  21276  lpiss  21362  zsssubrg  21466  qsssubdrg  21467  cnsubrg  21468  mulgrhm2  21512  znrrg  21607  ocvocv  21712  ocv2ss  21714  ocvin  21715  lsmcss  21733  cssmre  21734  pjcss  21759  lindfrn  21864  sraassab  21911  mhpsubg  22180  evls1maprnss  22403  dmatsgrp  22526  scmatsgrp  22546  scmatsgrp1  22549  m2cpmrngiso  22785  bastg  22994  tgss  22996  tgtop  23001  tgidm  23008  en2top  23013  neisspw  23136  topssnei  23153  neiptopuni  23159  lpss3  23173  clslp  23177  tgrest  23188  ssrest  23205  restntr  23211  ordtbas2  23220  ordtbas  23221  cnss1  23305  cnss2  23306  cnsscnp  23308  cnrest2r  23316  cmpsublem  23428  cmpsub  23429  tgcmp  23430  cmpcld  23431  hauscmplem  23435  cnconn  23451  llyss  23508  nllyss  23509  restnlly  23511  restlly  23512  locfincmp  23555  locfincf  23560  kgenss  23572  kgenidm  23576  llycmpkgen2  23579  1stckgen  23583  kgen2ss  23584  kgencn3  23587  ptbasfi  23610  ptpjopn  23641  txdis  23661  txkgen  23681  xkoptsub  23683  xkopjcn  23685  txconn  23718  qtoptop2  23728  qtopuni  23731  qtopkgen  23739  basqtop  23740  tgqtop  23741  qtopss  23744  qtoprest  23746  qtopomap  23747  qtopcmap  23748  kqsat  23760  kqcldsat  23762  hmphdis  23825  isfild  23887  ssfg  23901  fgss  23902  fgss2  23903  fgfil  23904  fgabs  23908  filconn  23912  fgtr  23919  uzrest  23926  ufilmax  23936  ufileu  23948  filufint  23949  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  flimss2  24001  flimss1  24002  flimclsi  24007  flimcf  24011  flimsncls  24015  fclssscls  24047  fclsss1  24051  fclsss2  24052  fclscf  24054  uffclsflim  24060  alexsublem  24073  alexsubALTlem3  24078  ptcmplem2  24082  ptcmplem3  24083  cnextf  24095  efmndtmd  24130  symgtgp  24135  cldsubg  24140  tsmscl  24164  haustsms2  24166  tgptsmscls  24179  tsmsxp  24184  restutop  24267  ustuqtop4  24274  utop2nei  24280  utop3cls  24281  ucncn  24315  xblss2ps  24432  xblss2  24433  xrsblre  24852  xrsmopn  24853  recld2  24855  zdis  24857  icccmplem2  24864  cncfss  24944  cnheiborlem  25005  htpycn  25024  phtpyhtpy  25033  pi1blem  25091  cphsscph  25304  cfilfcls  25327  iscmet3lem2  25345  iscmet2  25347  caussi  25350  equivcfil  25352  lmcau  25366  metsscmetcld  25368  hlhil  25496  ivthicc  25512  ovoliunnul  25561  ovolicopnf  25578  uniioombllem3  25639  dyadmbllem  25653  volsup2  25659  vitalilem2  25663  itg1addlem4  25753  itg1addlem4OLD  25754  itg10a  25765  itg1ge0a  25766  mbfi1fseqlem4  25773  itg2gt0  25815  limciun  25949  perfdvf  25958  cpnord  25991  dvcj  26008  dvlip2  26054  dvivth  26069  dvne0  26070  dvcnvre  26078  ply1lpir  26241  plyco0  26251  plyexmo  26373  abelth  26503  efif1o  26606  logno1  26696  efopnlem2  26717  loglesqrt  26822  lgamcvg2  27116  ppisval  27165  ppinprm  27213  chtnprm  27215  fsumvma  27275  dchrfi  27317  chtppilimlem2  27536  chebbnd2  27539  vmadivsumb  27545  rplogsumlem2  27547  dchrisumlem2  27552  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  selbergb  27611  selberg2b  27614  selberg3lem1  27619  selberg3lem2  27620  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  oldssmade  27934  sltlpss  27963  noseqrdgfn  28330  peano5uzs  28408  uhgredgss  29166  usgruspgrb  29218  uhgrissubgr  29310  uhgrspansubgrlem  29325  uhgrspan1  29338  cusgredg  29459  usgredgsscusgredg  29495  ococss  31325  shsub1  31356  shless  31391  shmodsi  31421  pjhth  31425  spansnss  31603  spanpr  31612  spansnm0i  31682  pjjsi  31732  sumdmdii  32447  sumdmdlem  32450  sumdmdlem2  32451  cdj3lem1  32466  abrexss  32540  fnpreimac  32689  rnmposs  32692  unifi3  32726  uzssico  32789  ssnnssfz  32792  pwrssmgc  32973  pmtrcnel  33082  cycpmrn  33136  cyc3evpm  33143  cycpmgcl  33146  fldgensdrg  33281  ringlsmss1  33389  ringlsmss2  33390  prmidlssidl  33438  mxidlirredi  33464  drngmxidl  33470  drngmxidlr  33471  1arithidomlem1  33528  1arithidom  33530  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  ply1mulrtss  33571  dimkerim  33640  extdg1id  33676  irngss  33687  irngssv  33688  algextdeglem8  33715  constrsscn  33730  constrsslem  33731  crefss  33795  cmpcref  33796  zarmxt1  33826  tpr2rico  33858  esumrnmpt2  34032  esumpcvgval  34042  ldsysgenld  34124  sigapildsys  34126  ldgenpisys  34130  cldssbrsiga  34151  measdivcstALTV  34189  mbfmcnt  34233  oddpwdc  34319  eulerpartlemgs2  34345  reprpmtf1o  34603  bnj1033  34945  bnj1398  35010  sconnpi1  35207  cvmscld  35241  cvmliftlem15  35266  satfrnmapom  35338  dfon2lem6  35752  fnessref  36323  fgmin  36336  tailfb  36343  dissneqlem  37306  icoreresf  37318  rdglimss  37343  finxpreclem6  37362  lindsenlbs  37575  poimirlem11  37591  poimirlem12  37592  sstotbnd3  37736  prdstotbnd  37754  cntotbnd  37756  ismtyhmeo  37765  1idl  37986  disjdmqsss  38758  lshpdisj  38943  lssats  38968  lkrin  39120  glbconxN  39335  paddss1  39774  paddss2  39775  paddasslem16  39792  paddidm  39798  pmodlem2  39804  pmapjoin  39809  pmapjat1  39810  pclfinN  39857  pclfinclN  39907  diasslssN  41016  dia2dimlem12  41032  dihsslss  41233  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  zndvdchrrhm  41927  dvrelog2  42021  dvrelog3  42022  aks4d1p3  42035  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8  42044  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  hashscontpow1  42078  aks6d1c4  42081  sticksstones3  42105  aks6d1c6lem3  42129  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  rhmqusspan  42142  unitscyglem1  42152  unitscyglem4  42155  ss2ab1  42212  eldiophss  42730  rencldnfilem  42776  pellexlem5  42789  pell14qrss1234  42812  pell1qrss14  42824  pellfundre  42837  pellfundge  42838  pellfundlb  42840  pellfundglb  42841  harinf  42991  proot1hash  43156  safesnsupfiss  43377  intabssd  43481  ss2iundf  43621  ov2ssiunov2  43662  clsk1indlem3  44005  finnzfsuppd  44171  radcnvrat  44283  nznngen  44285  trsspwALT3  44791  sspwimpALT2  44899  refsumcn  44930  iinssf  45040  icoiccdif  45442  icccncfext  45808  stoweidlem27  45948  stoweidlem46  45967  stoweidlem57  45978  fourierdlem40  46068  fourierdlem78  46105  ffnafv  47086  iccpartrn  47304  sprsymrelfvlem  47364  sprsymrelf1lem  47365  clnbgrssedg  47713  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  ssnn0ssfz  48074  lincolss  48163  lcoss  48165  lcosslsp  48167  iunord  48768