Theorem ssrdv 3939

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

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

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 3918

This theorem is referenced by:  eqelssd  3955  ss2abim  4012  ss2abdv  4017  sscon  4095  ssdif  4096  unss1  4137  ssrin  4194  eq0rdvALT  4360  sspw  4565  elpwdifsn  4745  uniss  4871  intss1  4918  intmin  4923  intssuni  4925  iinssiun  4960  iunss1  4961  iinss1  4962  ss2iun  4965  ssiun  5002  ssiun2  5003  iinss  5012  iinss2  5013  iunxdif3  5050  sspwb  5397  pwssun  5516  relop  5799  dmss  5851  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  imadifssran  6109  ssrnres  6136  sossfld  6144  predtrss  6280  preddowncl  6290  tron  6340  tz7.7  6343  funimassd  6900  dffv2  6929  chfnrn  6994  fvn0ssdmfun  7019  fveqdmss  7023  dff3  7045  ffnfv  7064  f1imass  7210  ssorduni  7724  onint  7735  limsssuc  7792  limuni3  7794  limomss  7813  fo1stres  7959  fo2ndres  7960  fo2ndf  8063  fnse  8075  ressuppssdif  8127  suppss  8136  reldmtpos  8176  fprlem2  8243  onfununi  8273  smoiun  8293  smocdmdom  8300  tz7.48-1  8374  tz7.49  8376  oaass  8488  cofon1  8600  cofon2  8601  qsss  8713  uniinqs  8734  pmss12g  8807  mapss  8827  ixpssmap2g  8865  ixpssmapg  8866  pssnn  9093  fineqv  9167  unifi3  9262  finnzfsuppd  9276  ssfii  9322  dffi2  9326  oismo  9445  unxpwdom2  9493  inf3lemd  9536  inf3lem1  9537  inf3lem6  9542  cantnflem3  9600  cantnf  9602  cnfcom3lem  9612  onssr1  9743  rankunb  9762  tcrank  9796  harcard  9890  carduni  9893  infxpenlem  9923  infpwfien  9972  dfac12r  10057  ackbij2lem1  10128  ackbij1lem18  10146  isfin1-3  10296  fin1a2lem11  10320  fin1a2lem13  10322  zorn2lem4  10409  zorn2lem5  10410  ttukeylem6  10424  ttukeylem7  10425  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe2  10554  wunr1om  10630  wunom  10631  tskr1om  10678  tskr1om2  10679  tskxpss  10683  tskcard  10692  tskuni  10694  grothomex  10740  genpss  10915  distrlem1pr  10936  distrlem5pr  10938  ltexprlem2  10948  ltexprlem6  10952  ltexprlem7  10953  reclem3pr  10960  reclem4pr  10961  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  peano5uzi  12581  uzss  12774  ixxdisj  13276  ixxss1  13279  ixxss2  13280  ixxss12  13281  ixxub  13282  ixxlb  13283  iocssre  13343  icossre  13344  iccssre  13345  icodisj  13392  fzss1  13479  fzss2  13480  ssfzunsnext  13485  fzosplit  13608  fzouzsplit  13610  ssfzo12bi  13677  ssnn0fi  13908  fsuppmapnn0fiub  13914  suppssfz  13917  sswrd  14445  rtrclreclem3  14983  isercoll  15591  summolem2a  15638  fsumcvg3  15652  fsum2dlem  15693  fsumcom2  15697  qshash  15750  prodmolem2a  15857  fprod2dlem  15903  fprodcom2  15907  bitsfzo  16362  1arith  16855  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  ramtlecl  16928  prmgaplem3  16981  prmgaplem4  16982  monhom  17659  epihom  17666  funcsetcres2  18017  funcestrcsetclem8  18070  funcsetcestrclem8  18085  psdmrn  18496  chnrss  18538  chndss  18539  gsumwspan  18771  frmdss2  18788  sursubmefmnd  18821  injsubmefmnd  18822  trivsubgsnd  19083  ssnmz  19095  trivnsgd  19101  kerf1ghm  19176  conjnmz  19181  symgvalstruct  19326  gex1  19520  sylow2alem1  19546  lsmless1x  19573  lsmless2x  19574  lsmub1x  19575  lsmub2x  19576  lsmmod  19604  lsmdisj2  19611  efgrelexlemb  19679  efgcpbllemb  19684  cntzcmn  19769  gsum2d2  19903  dprdub  19956  dprdss  19960  dprddisj2  19970  pgpfac1lem3  20008  subrngmre  20495  subrguss  20520  subrgmre  20530  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  rngcresringcat  20602  funcringcsetc  20607  unitrrg  20636  isdrng2  20676  primefld0cl  20739  primefld1cl  20740  lssssr  20905  lsssssubg  20909  lssmre  20917  lbspss  21034  lspdisj  21080  lbsextlem2  21114  lidl1el  21181  drngnidl  21198  lpiss  21284  zsssubrg  21380  qsssubdrg  21381  cnsubrg  21382  mulgrhm2  21433  znrrg  21520  ocvocv  21626  ocv2ss  21628  ocvin  21629  lsmcss  21647  cssmre  21648  pjcss  21671  lindfrn  21776  sraassab  21823  mhpsubg  22096  evls1maprnss  22322  dmatsgrp  22443  scmatsgrp  22463  scmatsgrp1  22466  m2cpmrngiso  22702  bastg  22910  tgss  22912  tgtop  22917  tgidm  22924  en2top  22929  neisspw  23051  topssnei  23068  neiptopuni  23074  lpss3  23088  clslp  23092  tgrest  23103  ssrest  23120  restntr  23126  ordtbas2  23135  ordtbas  23136  cnss1  23220  cnss2  23221  cnsscnp  23223  cnrest2r  23231  cmpsublem  23343  cmpsub  23344  tgcmp  23345  cmpcld  23346  hauscmplem  23350  cnconn  23366  llyss  23423  nllyss  23424  restnlly  23426  restlly  23427  locfincmp  23470  locfincf  23475  kgenss  23487  kgenidm  23491  llycmpkgen2  23494  1stckgen  23498  kgen2ss  23499  kgencn3  23502  ptbasfi  23525  ptpjopn  23556  txdis  23576  txkgen  23596  xkoptsub  23598  xkopjcn  23600  txconn  23633  qtoptop2  23643  qtopuni  23646  qtopkgen  23654  basqtop  23655  tgqtop  23656  qtopss  23659  qtoprest  23661  qtopomap  23662  qtopcmap  23663  kqsat  23675  kqcldsat  23677  hmphdis  23740  isfild  23802  ssfg  23816  fgss  23817  fgss2  23818  fgfil  23819  fgabs  23823  filconn  23827  fgtr  23834  uzrest  23841  ufilmax  23851  ufileu  23863  filufint  23864  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  flimss2  23916  flimss1  23917  flimclsi  23922  flimcf  23926  flimsncls  23930  fclssscls  23962  fclsss1  23966  fclsss2  23967  fclscf  23969  uffclsflim  23975  alexsublem  23988  alexsubALTlem3  23993  ptcmplem2  23997  ptcmplem3  23998  cnextf  24010  efmndtmd  24045  symgtgp  24050  cldsubg  24055  tsmscl  24079  haustsms2  24081  tgptsmscls  24094  tsmsxp  24099  restutop  24181  ustuqtop4  24188  utop2nei  24194  utop3cls  24195  ucncn  24228  xblss2ps  24345  xblss2  24346  xrsblre  24756  xrsmopn  24757  recld2  24759  zdis  24761  icccmplem2  24768  cncfss  24848  cnheiborlem  24909  htpycn  24928  phtpyhtpy  24937  pi1blem  24995  cphsscph  25207  cfilfcls  25230  iscmet3lem2  25248  iscmet2  25250  caussi  25253  equivcfil  25255  lmcau  25269  metsscmetcld  25271  hlhil  25399  ivthicc  25415  ovoliunnul  25464  ovolicopnf  25481  uniioombllem3  25542  dyadmbllem  25556  volsup2  25562  vitalilem2  25566  itg1addlem4  25656  itg10a  25667  itg1ge0a  25668  mbfi1fseqlem4  25675  itg2gt0  25717  limciun  25851  perfdvf  25860  cpnord  25893  dvcj  25910  dvlip2  25956  dvivth  25971  dvne0  25972  dvcnvre  25980  ply1lpir  26143  plyco0  26153  plyexmo  26277  abelth  26407  efif1o  26511  logno1  26601  efopnlem2  26622  loglesqrt  26727  lgamcvg2  27021  ppisval  27070  ppinprm  27118  chtnprm  27120  fsumvma  27180  dchrfi  27222  chtppilimlem2  27441  chebbnd2  27444  vmadivsumb  27450  rplogsumlem2  27452  dchrisumlem2  27457  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  selbergb  27516  selberg2b  27519  selberg3lem1  27524  selberg3lem2  27525  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  oldssmade  27863  ltslpss  27904  noseqrdgfn  28302  n0ssoldg  28349  peano5uzs  28400  uhgredgss  29204  usgruspgrb  29256  uhgrissubgr  29348  uhgrspansubgrlem  29363  uhgrspan1  29376  cusgredg  29497  usgredgsscusgredg  29533  ococss  31368  shsub1  31399  shless  31434  shmodsi  31464  pjhth  31468  spansnss  31646  spanpr  31655  spansnm0i  31725  pjjsi  31775  sumdmdii  32490  sumdmdlem  32493  sumdmdlem2  32494  cdj3lem1  32509  abrexss  32587  fnpreimac  32749  rnmposs  32752  uzssico  32864  ssnnssfz  32867  pwrssmgc  33082  pmtrcnel  33171  cycpmrn  33225  cyc3evpm  33232  cycpmgcl  33235  elrgspnlem1  33324  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem2  33330  fldgensdrg  33396  ringlsmss1  33477  ringlsmss2  33478  prmidlssidl  33526  mxidlirredi  33552  drngmxidl  33558  drngmxidlr  33559  1arithidomlem1  33616  1arithidom  33618  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  ply1mulrtss  33663  dimkerim  33784  extdg1id  33823  irngss  33844  irngssv  33845  algextdeglem8  33881  constrsscn  33897  constrsslem  33898  constrsdrg  33932  crefss  34006  cmpcref  34007  zarmxt1  34037  tpr2rico  34069  esumrnmpt2  34225  esumpcvgval  34235  ldsysgenld  34317  sigapildsys  34319  ldgenpisys  34323  cldssbrsiga  34344  measdivcstALTV  34382  mbfmcnt  34425  oddpwdc  34511  eulerpartlemgs2  34537  reprpmtf1o  34783  bnj1033  35125  bnj1398  35190  trssfir1om  35267  r1omhfb  35268  trssfir1omregs  35292  r1omhfbregs  35293  sconnpi1  35433  cvmscld  35467  cvmliftlem15  35492  satfrnmapom  35564  dfon2lem6  35980  fnessref  36551  fgmin  36564  tailfb  36571  dissneqlem  37545  icoreresf  37557  rdglimss  37582  finxpreclem6  37601  lindsenlbs  37816  poimirlem11  37832  poimirlem12  37833  sstotbnd3  37977  prdstotbnd  37995  cntotbnd  37997  ismtyhmeo  38006  1idl  38227  disjdmqsss  39061  lshpdisj  39247  lssats  39272  lkrin  39424  glbconxN  39638  paddss1  40077  paddss2  40078  paddasslem16  40095  paddidm  40101  pmodlem2  40107  pmapjoin  40112  pmapjat1  40113  pclfinN  40160  pclfinclN  40210  diasslssN  41319  dia2dimlem12  41335  dihsslss  41536  baerlem3lem2  41970  baerlem5alem2  41971  baerlem5blem2  41972  zndvdchrrhm  42226  dvrelog2  42318  dvrelog3  42319  aks4d1p3  42332  aks4d1p4  42333  aks4d1p5  42334  aks4d1p7  42337  aks4d1p8  42341  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  hashscontpow1  42375  aks6d1c4  42378  sticksstones3  42402  aks6d1c6lem3  42426  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  rhmqusspan  42439  unitscyglem1  42449  unitscyglem4  42452  eldiophss  43016  rencldnfilem  43062  pellexlem5  43075  pell14qrss1234  43098  pell1qrss14  43110  pellfundre  43123  pellfundge  43124  pellfundlb  43126  pellfundglb  43127  harinf  43276  proot1hash  43437  safesnsupfiss  43656  intabssd  43760  ss2iundf  43900  ov2ssiunov2  43941  clsk1indlem3  44284  radcnvrat  44555  nznngen  44557  trsspwALT3  45060  sspwimpALT2  45168  refsumcn  45275  iinssf  45382  icoiccdif  45770  icccncfext  46131  stoweidlem27  46271  stoweidlem46  46290  stoweidlem57  46301  fourierdlem40  46391  fourierdlem78  46428  ffnafv  47417  iccpartrn  47676  sprsymrelfvlem  47736  sprsymrelf1lem  47737  clnbgrssedg  48087  stgrusgra  48205  rhmsubcALTVlem4  48530  funcringcsetcALTV2lem8  48543  funcringcsetclem8ALTV  48566  ssnn0ssfz  48595  lincolss  48680  lcoss  48682  lcosslsp  48684  iunord  49921