Theorem ssrdv 3919

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2147   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

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

This theorem is used by:  eqelssd  3934  ss2abim  3988  ss2abdv  3993  sscon  4082  ssdif  4083  ssrin  4141  unss1  4186  eq0rdvALT  4369  sspw  4571  elpwdifsn  4754  uniss  4880  intss1  4928  intmin  4933  intssuni  4935  iinssiun  4970  iunss1  4971  iinss1  4972  ss2iun  4975  ssiun  5010  ssiun2  5011  iinss  5020  iinss2  5021  iunxdif3  5060  sspwb  5424  pwssun  5550  ssrel  5767  relop  5838  dmss  5896  dmcosseq  5972  dmcosseqOLD  5973  ssrnres  6188  sossfld  6196  imadifssranOLD  6221  imadifssranOLDOLD  6222  predtrss  6351  preddowncl  6361  tron  6411  tz7.7  6414  funimassd  6982  dffv2  7011  chfnrn  7079  fvn0ssdmfun  7106  fveqdmss  7110  dff3  7132  ffnfv  7151  f1imass  7299  rnmposs  7586  ssorduni  7827  onint  7838  limsssuc  7895  limuni3  7897  limomss  7916  fo1stres  8061  fo2ndres  8062  fo2ndf  8169  fnse  8187  ressuppssdif  8240  suppss  8249  reldmtpos  8289  fprlem2  8357  onfununi  8387  smoiun  8407  smocdmdom  8414  tz7.48-1  8491  tz7.49  8493  oaass  8607  cofon1  8719  cofon2  8720  qsss  8834  uniinqs  8856  pmss12g  8935  mapss  8955  ixpssmap2g  8993  ixpssmapg  8994  pssnn  9222  fineqv  9296  unifi3  9389  finnzfsuppd  9402  ssfii  9448  dffi2  9452  oismo  9571  unxpwdom2  9619  inf3lemd  9665  inf3lem1  9666  inf3lem6  9671  cantnflem3  9729  cantnf  9731  cnfcom3lem  9741  onssr1  9880  rankunb  9901  tcrank  9938  elhf3OLD  9960  harcard  10096  carduni  10101  infxpenlem  10131  infpwfien  10180  dfac12r  10264  ackbij2lem1  10335  ackbij1lem18  10353  isfin1-3  10503  fin1a2lem11  10527  fin1a2lem13  10529  zorn2lem4  10616  zorn2lem5  10617  ttukeylem6  10631  ttukeylem7  10632  fpwwe2lem10  10764  fpwwe2lem11  10765  fpwwe2  10767  wunr1om  10843  wunom  10844  tskr1om  10891  tskhf  10892  tskxpss  10896  tskcard  10905  tskuni  10907  grothomex  10953  genpss  11128  distrlem1pr  11149  distrlem5pr  11151  ltexprlem2  11161  ltexprlem6  11165  ltexprlem7  11166  reclem3pr  11173  reclem4pr  11174  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  peano5uzi  12828  uzss  13028  ixxdisj  13531  ixxss1  13534  ixxss2  13535  ixxss12  13536  ixxub  13537  ixxlb  13538  iocssre  13598  icossre  13599  iccssre  13600  icodisj  13647  fzss1  13737  fzss2  13738  ssfzunsnext  13743  fzosplit  13867  fzouzsplit  13869  ssfzo12bi  13936  ssnn0fi  14168  fsuppmapnn0fiub  14174  suppssfz  14177  sswrd  14708  rtrclreclem3  15256  isercoll  15879  summolem2a  15925  fsumcvg3  15939  fsum2dlem  15980  fsumcom2  15984  qshash  16038  prodmolem2a  16145  fprod2dlem  16191  fprodcom2  16195  bitsfzo  16649  1arith  17149  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  ramtlecl  17222  prmgaplem3  17275  prmgaplem4  17276  monhom  17960  epihom  17967  funcsetcres2  18318  funcestrcsetclem8  18371  funcsetcestrclem8  18386  psdmrn  18797  chnrss  18839  chndss  18840  gsumwspan  19092  frmdss2  19109  sursubmefmnd  19142  injsubmefmnd  19143  trivsubgsnd  19414  ssnmz  19426  trivnsgd  19432  kerf1ghm  19511  conjnmz  19516  symgvalstruct  19662  gex1  19856  sylow2alem1  19882  lsmless1x  19909  lsmless2x  19910  lsmub1x  19911  lsmub2x  19912  lsmmod  19940  lsmdisj2  19947  efgrelexlemb  20015  efgcpbllemb  20020  cntzcmn  20105  gsum2d2  20239  dprdub  20292  dprdss  20296  dprddisj2  20306  pgpfac1lem3  20344  subrngmre  20865  subrguss  20890  subrgmre  20900  rnghmsscmap2  20932  rnghmsscmap  20933  funcrngcsetc  20943  funcrngcsetcALT  20944  rhmsscmap2  20961  rhmsscmap  20962  rhmsscrnghm  20968  rngcresringcat  20972  funcringcsetc  20977  unitrrg  21006  isdrng2  21048  primefld0cl  21114  primefld1cl  21115  lssssr  21280  lsssssubg  21284  lssmre  21292  lbspss  21408  lspdisj  21454  lbsextlem2  21488  lidl1el  21556  drngnidl  21582  prmidlssidl  21677  lpiss  21704  zsssubrg  21785  qsssubdrg  21786  cnsubrg  21787  mulgrhm2  21839  znrrg  21926  ocvocv  22032  ocv2ss  22034  ocvin  22035  lsmcss  22053  cssmre  22054  pjcss  22077  lindfrn  22182  lindsenlbs  22212  sraassab  22231  mhpsubg  22529  evls1maprnss  22751  dmatsgrp  22869  scmatsgrp  22889  scmatsgrp1  22892  m2cpmrngiso  23131  bastg  23339  tgss  23341  tgtop  23346  tgidm  23353  en2top  23358  neisspw  23480  topssnei  23497  neiptopuni  23503  lpss3  23517  clslp  23521  tgrest  23532  ssrest  23549  restntr  23555  ordtbas2  23564  ordtbas  23565  cnss1  23649  cnss2  23650  cnsscnp  23652  cnrest2r  23660  cmpsublem  23772  cmpsub  23773  tgcmp  23774  cmpcld  23775  hauscmplem  23779  cnconn  23795  llyss  23853  nllyss  23854  restnlly  23856  restlly  23857  locfincmp  23900  locfincf  23905  kgenss  23917  kgenidm  23921  llycmpkgen2  23924  1stckgen  23928  kgen2ss  23929  kgencn3  23932  ptbasfi  23955  ptpjopn  23986  txdis  24006  txkgen  24026  xkoptsub  24028  xkopjcn  24030  txconn  24063  qtoptop2  24073  qtopuni  24076  qtopkgen  24084  basqtop  24085  tgqtop  24086  qtopss  24089  qtoprest  24091  qtopomap  24092  qtopcmap  24093  kqsat  24105  kqcldsat  24107  hmphdis  24170  isfild  24232  ssfg  24246  fgss  24247  fgss2  24248  fgfil  24249  fgabs  24253  filconn  24257  fgtr  24264  uzrest  24271  ufilmax  24281  ufileu  24293  filufint  24294  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem4  24331  flimss2  24346  flimss1  24347  flimclsi  24352  flimcf  24356  flimsncls  24360  fclssscls  24392  fclsss1  24396  fclsss2  24397  fclscf  24399  uffclsflim  24405  alexsublem  24418  alexsubALTlem3  24423  ptcmplem2  24427  ptcmplem3  24428  cnextf  24440  efmndtmd  24475  symgtgp  24480  cldsubg  24485  tsmscl  24509  haustsms2  24511  tgptsmscls  24524  tsmsxp  24529  restutop  24611  ustuqtop4  24618  utop2nei  24624  utop3cls  24625  ucncn  24658  xblss2ps  24775  xblss2  24776  xrsblre  25186  xrsmopn  25187  recld2  25189  zdis  25191  icccmplem2  25198  cncfss  25275  cnheiborlem  25330  htpycn  25349  phtpyhtpy  25358  pi1blem  25415  cphsscph  25627  cfilfcls  25650  iscmet3lem2  25668  iscmet2  25670  caussi  25673  equivcfil  25675  lmcau  25689  metsscmetcld  25691  hlhil  25819  ivthicc  25834  ovoliunnul  25883  ovolicopnf  25900  uniioombllem3  25961  dyadmbllem  25975  volsup2  25981  vitalilem2  25985  itg1addlem4  26075  itg10a  26086  itg1ge0a  26087  mbfi1fseqlem4  26094  itg2gt0  26136  limciun  26269  perfdvf  26278  cpnord  26310  dvcj  26325  dvlip2  26370  dvivth  26385  dvne0  26386  dvcnvre  26394  ply1lpir  26555  plyco0  26565  plyconz  26686  plyexmo  26691  abelth  26825  efif1o  26931  logno1  27021  efopnlem2  27042  loglesqrt  27146  lgamcvg2  27439  ppisval  27488  ppinprm  27536  chtnprm  27538  fsumvma  27597  dchrfi  27639  chtppilimlem2  27858  chebbnd2  27861  vmadivsumb  27867  rplogsumlem2  27869  dchrisumlem2  27874  vmalogdivsum2  27922  vmalogdivsum  27923  2vmadivsumlem  27924  selbergb  27933  selberg2b  27936  selberg3lem1  27941  selberg3lem2  27942  selberg3  27943  selberg4lem1  27944  selberg4  27945  pntrlog2bndlem2  27962  pntrlog2bndlem4  27964  oldssmade  28310  ltslpss  28351  noseqrdgfn  28749  n0ssoldg  28796  peano5uzs  28847  elplnglnid  29318  lnincplng  29319  plngrotlem2  29323  cgrabasimass  29435  prlngpln3  29484  uhgredgss  29766  usgruspgrb  29821  uhgrissubgr  29913  uhgrspansubgrlem  29928  uhgrspan1  29941  cusgredg  30062  usgredgsscusgredg  30097  ococss  31952  shsub1  31983  shless  32018  shmodsi  32048  pjhth  32052  spansnss  32230  spanpr  32239  spansnm0i  32309  pjjsi  32359  sumdmdii  33074  sumdmdlem  33077  sumdmdlem2  33078  cdj3lem1  33093  abrexss  33207  fnpreimac  33362  uzssico  33472  ssnnssfz  33475  pwrssmgc  33660  pmtrcnel  33749  cycpmrn  33803  cyc3evpm  33810  cycpmgcl  33813  elrgspnlem1  33902  elrgspnlem3  33904  elrgspnlem4  33905  elrgspnsubrunlem2  33908  edompidlem  33960  edompid  33961  fldgensdrg  33980  ringlsmss1  34053  ringlsmss2  34054  mxidlirredi  34100  drngmxidl  34105  drngmxidlr  34106  1arithidomlem1  34171  1arithidom  34173  1arithufdlem2  34181  1arithufdlem3  34182  1arithufdlem4  34183  dfufd2lem  34185  ply1mulrtss  34217  esplyfvaln  34317  dimkerim  34370  extdg1id  34409  irngss  34430  irngssv  34431  algextdeglem8  34467  constrsscn  34483  constrsslem  34484  constrsdrg  34518  crefss  34592  cmpcref  34593  zarmxt1  34623  tpr2rico  34655  esumrnmpt2  34811  esumpcvgval  34821  ldsysgenld  34904  sigapildsys  34906  ldgenpisys  34910  cldssbrsiga  34931  measdivcstALTV  34969  mbfmcnt  35011  oddpwdc  35097  eulerpartlemgs2  35123  reprpmtf1o  35366  bnj1033  35710  bnj1398  35775  trssfihf  35860  eqhf  35861  acwer1prc  35893  trssfihfregs  35945  eqhfregs  35946  sconnpi1  36212  cvmscld  36246  cvmliftlem15  36271  satfrnmapom  36343  dfon2lem6  36765  fnessref  37360  fgmin  37373  tailfb  37380  bj-ssrel  38175  dissneqlem  38531  icoreresf  38543  rdglimss  38568  finxpreclem6  38587  poimirlem11  38817  poimirlem12  38818  sstotbnd3  38976  prdstotbnd  38994  cntotbnd  38996  ismtyhmeo  39005  1idl  39226  disjdmqsss  40103  lshpdisj  40310  lssats  40335  lkrin  40487  glbconxN  40701  paddss1  41140  paddss2  41141  paddasslem16  41158  paddidm  41164  pmodlem2  41170  pmapjoin  41175  pmapjat1  41176  pclfinN  41223  pclfinclN  41273  diasslssN  42382  dia2dimlem12  42398  dihsslss  42599  baerlem3lem2  43033  baerlem5alem2  43034  baerlem5blem2  43035  zndvdchrrhm  43289  dvrelog2  43380  dvrelog3  43381  aks4d1p3  43394  aks4d1p4  43395  aks4d1p5  43396  aks4d1p7  43399  aks4d1p8  43403  primrootsunit1  43413  primrootscoprmpow  43415  primrootscoprbij  43418  hashscontpow1  43437  aks6d1c4  43440  sticksstones3  43464  aks6d1c6lem3  43488  aks6d1c6isolem2  43491  aks6d1c6lem5  43493  rhmqusspan  43501  unitscyglem1  43511  unitscyglem4  43514  eldiophss  44051  rencldnfilem  44093  pellexlem5  44106  pell14qrss1234  44129  pell1qrss14  44141  pellfundre  44154  pellfundge  44155  pellfundlb  44157  pellfundglb  44158  harinf  44307  proot1hash  44458  safesnsupfiss  44677  intabssd  44781  ss2iundf  44920  ov2ssiunov2  44961  clsk1indlem3  45304  radcnvrat  45559  nznngen  45561  trsspwALT3  46062  sspwimpALT2  46170  refsumcn  46321  iinssf  46426  icoiccdif  46809  icccncfext  47170  stoweidlem27  47310  stoweidlem46  47329  stoweidlem57  47340  fourierdlem40  47430  fourierdlem78  47467  ffnafv  48514  iccpartrn  48785  sprsymrelfvlem  48845  sprsymrelf1lem  48846  clnbgrssedg  49212  stgrusgra  49330  rhmsubcALTVlem4  49654  funcringcsetcALTV2lem8  49667  funcringcsetclem8ALTV  49690  lazssaz  49730  ssnn0ssfz  49792  lincolss  49877  lcoss  49879  lcosslsp  49881  iunord  51190