Theorem ssrdv 3915

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ss 3897

This theorem is used by:  eqelssd  3930  ss2abim  3984  ss2abdv  3989  sscon  4078  ssdif  4079  ssrin  4137  unss1  4182  eq0rdvALT  4365  sspw  4567  elpwdifsn  4748  uniss  4874  intss1  4922  intmin  4927  intssuni  4929  iinssiun  4964  iunss1  4965  iinss1  4966  ss2iun  4969  ssiun  5004  ssiun2  5005  iinss  5014  iinss2  5015  iunxdif3  5054  sspwb  5417  pwssun  5543  relop  5829  dmss  5885  dmcosseq  5961  dmcosseqOLD  5962  ssrnres  6172  sossfld  6180  imadifssranOLD  6205  imadifssranOLDOLD  6206  predtrss  6328  preddowncl  6338  tron  6388  tz7.7  6391  funimassd  6956  dffv2  6985  chfnrn  7053  fvn0ssdmfun  7079  fveqdmss  7083  dff3  7105  ffnfv  7124  f1imass  7272  ssorduni  7797  onint  7808  limsssuc  7865  limuni3  7867  limomss  7886  fo1stres  8031  fo2ndres  8032  fo2ndf  8138  fnse  8156  ressuppssdif  8209  suppss  8218  reldmtpos  8258  fprlem2  8326  onfununi  8356  smoiun  8376  smocdmdom  8383  tz7.48-1  8460  tz7.49  8462  oaass  8576  cofon1  8688  cofon2  8689  qsss  8803  uniinqs  8825  pmss12g  8904  mapss  8924  ixpssmap2g  8962  ixpssmapg  8963  pssnn  9191  fineqv  9265  unifi3  9358  finnzfsuppd  9372  ssfii  9418  dffi2  9422  oismo  9541  unxpwdom2  9589  inf3lemd  9635  inf3lem1  9636  inf3lem6  9641  cantnflem3  9699  cantnf  9701  cnfcom3lem  9711  onssr1  9850  rankunb  9871  tcrank  9908  elhf3OLD  9930  harcard  10066  carduni  10069  infxpenlem  10099  infpwfien  10148  dfac12r  10232  ackbij2lem1  10303  ackbij1lem18  10321  isfin1-3  10471  fin1a2lem11  10495  fin1a2lem13  10497  zorn2lem4  10584  zorn2lem5  10585  ttukeylem6  10599  ttukeylem7  10600  fpwwe2lem10  10732  fpwwe2lem11  10733  fpwwe2  10735  wunr1om  10811  wunom  10812  tskr1om  10859  tskhf  10860  tskxpss  10864  tskcard  10873  tskuni  10875  grothomex  10921  genpss  11096  distrlem1pr  11117  distrlem5pr  11119  ltexprlem2  11129  ltexprlem6  11133  ltexprlem7  11134  reclem3pr  11141  reclem4pr  11142  supaddc  12291  supadd  12292  supmul1  12293  supmullem2  12295  peano5uzi  12795  uzss  12995  ixxdisj  13498  ixxss1  13501  ixxss2  13502  ixxss12  13503  ixxub  13504  ixxlb  13505  iocssre  13565  icossre  13566  iccssre  13567  icodisj  13614  fzss1  13704  fzss2  13705  ssfzunsnext  13710  fzosplit  13834  fzouzsplit  13836  ssfzo12bi  13903  ssnn0fi  14135  fsuppmapnn0fiub  14141  suppssfz  14144  sswrd  14674  rtrclreclem3  15222  isercoll  15844  summolem2a  15890  fsumcvg3  15904  fsum2dlem  15945  fsumcom2  15949  qshash  16003  prodmolem2a  16110  fprod2dlem  16156  fprodcom2  16160  bitsfzo  16614  1arith  17114  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  ramtlecl  17187  prmgaplem3  17240  prmgaplem4  17241  monhom  17919  epihom  17926  funcsetcres2  18277  funcestrcsetclem8  18330  funcsetcestrclem8  18345  psdmrn  18756  chnrss  18798  chndss  18799  gsumwspan  19051  frmdss2  19068  sursubmefmnd  19101  injsubmefmnd  19102  trivsubgsnd  19373  ssnmz  19385  trivnsgd  19391  kerf1ghm  19470  conjnmz  19475  symgvalstruct  19620  gex1  19814  sylow2alem1  19840  lsmless1x  19867  lsmless2x  19868  lsmub1x  19869  lsmub2x  19870  lsmmod  19898  lsmdisj2  19905  efgrelexlemb  19973  efgcpbllemb  19978  cntzcmn  20063  gsum2d2  20197  dprdub  20250  dprdss  20254  dprddisj2  20264  pgpfac1lem3  20302  subrngmre  20823  subrguss  20848  subrgmre  20858  rnghmsscmap2  20890  rnghmsscmap  20891  funcrngcsetc  20901  funcrngcsetcALT  20902  rhmsscmap2  20919  rhmsscmap  20920  rhmsscrnghm  20926  rngcresringcat  20930  funcringcsetc  20935  unitrrg  20964  isdrng2  21006  primefld0cl  21072  primefld1cl  21073  lssssr  21238  lsssssubg  21242  lssmre  21250  lbspss  21366  lspdisj  21412  lbsextlem2  21446  lidl1el  21514  drngnidl  21540  prmidlssidl  21635  lpiss  21662  zsssubrg  21740  qsssubdrg  21741  cnsubrg  21742  mulgrhm2  21793  znrrg  21880  ocvocv  21986  ocv2ss  21988  ocvin  21989  lsmcss  22007  cssmre  22008  pjcss  22031  lindfrn  22136  lindsenlbs  22166  sraassab  22185  mhpsubg  22483  evls1maprnss  22705  dmatsgrp  22823  scmatsgrp  22843  scmatsgrp1  22846  m2cpmrngiso  23085  bastg  23293  tgss  23295  tgtop  23300  tgidm  23307  en2top  23312  neisspw  23434  topssnei  23451  neiptopuni  23457  lpss3  23471  clslp  23475  tgrest  23486  ssrest  23503  restntr  23509  ordtbas2  23518  ordtbas  23519  cnss1  23603  cnss2  23604  cnsscnp  23606  cnrest2r  23614  cmpsublem  23726  cmpsub  23727  tgcmp  23728  cmpcld  23729  hauscmplem  23733  cnconn  23749  llyss  23807  nllyss  23808  restnlly  23810  restlly  23811  locfincmp  23854  locfincf  23859  kgenss  23871  kgenidm  23875  llycmpkgen2  23878  1stckgen  23882  kgen2ss  23883  kgencn3  23886  ptbasfi  23909  ptpjopn  23940  txdis  23960  txkgen  23980  xkoptsub  23982  xkopjcn  23984  txconn  24017  qtoptop2  24027  qtopuni  24030  qtopkgen  24038  basqtop  24039  tgqtop  24040  qtopss  24043  qtoprest  24045  qtopomap  24046  qtopcmap  24047  kqsat  24059  kqcldsat  24061  hmphdis  24124  isfild  24186  ssfg  24200  fgss  24201  fgss2  24202  fgfil  24203  fgabs  24207  filconn  24211  fgtr  24218  uzrest  24225  ufilmax  24235  ufileu  24247  filufint  24248  rnelfm  24281  fmfnfmlem2  24283  fmfnfmlem4  24285  flimss2  24300  flimss1  24301  flimclsi  24306  flimcf  24310  flimsncls  24314  fclssscls  24346  fclsss1  24350  fclsss2  24351  fclscf  24353  uffclsflim  24359  alexsublem  24372  alexsubALTlem3  24377  ptcmplem2  24381  ptcmplem3  24382  cnextf  24394  efmndtmd  24429  symgtgp  24434  cldsubg  24439  tsmscl  24463  haustsms2  24465  tgptsmscls  24478  tsmsxp  24483  restutop  24565  ustuqtop4  24572  utop2nei  24578  utop3cls  24579  ucncn  24612  xblss2ps  24729  xblss2  24730  xrsblre  25140  xrsmopn  25141  recld2  25143  zdis  25145  icccmplem2  25152  cncfss  25229  cnheiborlem  25284  htpycn  25303  phtpyhtpy  25312  pi1blem  25369  cphsscph  25581  cfilfcls  25604  iscmet3lem2  25622  iscmet2  25624  caussi  25627  equivcfil  25629  lmcau  25643  metsscmetcld  25645  hlhil  25773  ivthicc  25788  ovoliunnul  25837  ovolicopnf  25854  uniioombllem3  25915  dyadmbllem  25929  volsup2  25935  vitalilem2  25939  itg1addlem4  26029  itg10a  26040  itg1ge0a  26041  mbfi1fseqlem4  26048  itg2gt0  26090  limciun  26223  perfdvf  26232  cpnord  26264  dvcj  26279  dvlip2  26324  dvivth  26339  dvne0  26340  dvcnvre  26348  ply1lpir  26509  plyco0  26519  plyconz  26640  plyexmo  26645  abelth  26777  efif1o  26883  logno1  26973  efopnlem2  26994  loglesqrt  27098  lgamcvg2  27391  ppisval  27440  ppinprm  27488  chtnprm  27490  fsumvma  27549  dchrfi  27591  chtppilimlem2  27810  chebbnd2  27813  vmadivsumb  27819  rplogsumlem2  27821  dchrisumlem2  27826  vmalogdivsum2  27874  vmalogdivsum  27875  2vmadivsumlem  27876  selbergb  27885  selberg2b  27888  selberg3lem1  27893  selberg3lem2  27894  selberg3  27895  selberg4lem1  27896  selberg4  27897  pntrlog2bndlem2  27914  pntrlog2bndlem4  27916  oldssmade  28262  ltslpss  28303  noseqrdgfn  28701  n0ssoldg  28748  peano5uzs  28799  elplnglnid  29270  lnincplng  29271  plngrotlem2  29275  cgrabasimass  29387  prlngpln3  29436  uhgredgss  29718  usgruspgrb  29773  uhgrissubgr  29865  uhgrspansubgrlem  29880  uhgrspan1  29893  cusgredg  30014  usgredgsscusgredg  30049  ococss  31904  shsub1  31935  shless  31970  shmodsi  32000  pjhth  32004  spansnss  32182  spanpr  32191  spansnm0i  32261  pjjsi  32311  sumdmdii  33026  sumdmdlem  33029  sumdmdlem2  33030  cdj3lem1  33045  abrexss  33159  fnpreimac  33315  rnmposs  33318  uzssico  33426  ssnnssfz  33429  pwrssmgc  33611  pmtrcnel  33700  cycpmrn  33754  cyc3evpm  33761  cycpmgcl  33764  elrgspnlem1  33853  elrgspnlem3  33855  elrgspnlem4  33856  elrgspnsubrunlem2  33859  fldgensdrg  33926  ringlsmss1  33999  ringlsmss2  34000  mxidlirredi  34046  drngmxidl  34051  drngmxidlr  34052  1arithidomlem1  34117  1arithidom  34119  1arithufdlem2  34127  1arithufdlem3  34128  1arithufdlem4  34129  dfufd2lem  34131  ply1mulrtss  34164  esplyfvaln  34256  dimkerim  34309  extdg1id  34348  irngss  34369  irngssv  34370  algextdeglem8  34406  constrsscn  34422  constrsslem  34423  constrsdrg  34457  crefss  34531  cmpcref  34532  zarmxt1  34562  tpr2rico  34594  esumrnmpt2  34750  esumpcvgval  34760  ldsysgenld  34843  sigapildsys  34845  ldgenpisys  34849  cldssbrsiga  34870  measdivcstALTV  34908  mbfmcnt  34950  oddpwdc  35036  eulerpartlemgs2  35062  reprpmtf1o  35305  bnj1033  35649  bnj1398  35714  trssfir1om  35793  r1omhfb  35794  acwer1prc  35820  trssfir1omregs  35864  r1omhfbregs  35865  sconnpi1  36094  cvmscld  36128  cvmliftlem15  36153  satfrnmapom  36225  dfon2lem6  36646  fnessref  37241  fgmin  37254  tailfb  37261  dissneqlem  38372  icoreresf  38384  rdglimss  38409  finxpreclem6  38428  poimirlem11  38658  poimirlem12  38659  sstotbnd3  38819  prdstotbnd  38837  cntotbnd  38839  ismtyhmeo  38848  1idl  39069  disjdmqsss  39946  lshpdisj  40153  lssats  40178  lkrin  40330  glbconxN  40544  paddss1  40983  paddss2  40984  paddasslem16  41001  paddidm  41007  pmodlem2  41013  pmapjoin  41018  pmapjat1  41019  pclfinN  41066  pclfinclN  41116  diasslssN  42225  dia2dimlem12  42241  dihsslss  42442  baerlem3lem2  42876  baerlem5alem2  42877  baerlem5blem2  42878  zndvdchrrhm  43132  dvrelog2  43223  dvrelog3  43224  aks4d1p3  43237  aks4d1p4  43238  aks4d1p5  43239  aks4d1p7  43242  aks4d1p8  43246  primrootsunit1  43256  primrootscoprmpow  43258  primrootscoprbij  43261  hashscontpow1  43280  aks6d1c4  43283  sticksstones3  43307  aks6d1c6lem3  43331  aks6d1c6isolem2  43334  aks6d1c6lem5  43336  rhmqusspan  43344  unitscyglem1  43354  unitscyglem4  43357  eldiophss  43894  rencldnfilem  43936  pellexlem5  43949  pell14qrss1234  43972  pell1qrss14  43984  pellfundre  43997  pellfundge  43998  pellfundlb  44000  pellfundglb  44001  harinf  44150  proot1hash  44306  safesnsupfiss  44525  intabssd  44629  ss2iundf  44768  ov2ssiunov2  44809  clsk1indlem3  45152  radcnvrat  45407  nznngen  45409  trsspwALT3  45910  sspwimpALT2  46018  refsumcn  46155  iinssf  46261  icoiccdif  46644  icccncfext  47005  stoweidlem27  47145  stoweidlem46  47164  stoweidlem57  47175  fourierdlem40  47265  fourierdlem78  47302  ffnafv  48349  iccpartrn  48620  sprsymrelfvlem  48680  sprsymrelf1lem  48681  clnbgrssedg  49047  stgrusgra  49165  rhmsubcALTVlem4  49489  funcringcsetcALTV2lem8  49502  funcringcsetclem8ALTV  49525  ssnn0ssfz  49569  lincolss  49654  lcoss  49656  lcosslsp  49658  iunord  50967