Theorem ssrdv 3928

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  eqelssd  3944  ss2abim  4001  ss2abdv  4006  sscon  4084  ssdif  4085  unss1  4126  ssrin  4183  eq0rdvALT  4349  sspw  4553  elpwdifsn  4733  uniss  4859  intss1  4906  intmin  4911  intssuni  4913  iinssiun  4948  iunss1  4949  iinss1  4950  ss2iun  4953  ssiun  4990  ssiun2  4991  iinss  5000  iinss2  5001  iunxdif3  5038  sspwb  5396  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  6995  fvn0ssdmfun  7020  fveqdmss  7024  dff3  7046  ffnfv  7065  f1imass  7212  ssorduni  7726  onint  7737  limsssuc  7794  limuni3  7796  limomss  7815  fo1stres  7961  fo2ndres  7962  fo2ndf  8064  fnse  8076  ressuppssdif  8128  suppss  8137  reldmtpos  8177  fprlem2  8244  onfununi  8274  smoiun  8294  smocdmdom  8301  tz7.48-1  8375  tz7.49  8377  oaass  8489  cofon1  8601  cofon2  8602  qsss  8715  uniinqs  8737  pmss12g  8810  mapss  8830  ixpssmap2g  8868  ixpssmapg  8869  pssnn  9096  fineqv  9170  unifi3  9265  finnzfsuppd  9279  ssfii  9325  dffi2  9329  oismo  9448  unxpwdom2  9496  inf3lemd  9539  inf3lem1  9540  inf3lem6  9545  cantnflem3  9603  cantnf  9605  cnfcom3lem  9615  onssr1  9746  rankunb  9765  tcrank  9799  harcard  9893  carduni  9896  infxpenlem  9926  infpwfien  9975  dfac12r  10060  ackbij2lem1  10131  ackbij1lem18  10149  isfin1-3  10299  fin1a2lem11  10323  fin1a2lem13  10325  zorn2lem4  10412  zorn2lem5  10413  ttukeylem6  10427  ttukeylem7  10428  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2  10557  wunr1om  10633  wunom  10634  tskr1om  10681  tskr1om2  10682  tskxpss  10686  tskcard  10695  tskuni  10697  grothomex  10743  genpss  10918  distrlem1pr  10939  distrlem5pr  10941  ltexprlem2  10951  ltexprlem6  10955  ltexprlem7  10956  reclem3pr  10963  reclem4pr  10964  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  peano5uzi  12609  uzss  12802  ixxdisj  13304  ixxss1  13307  ixxss2  13308  ixxss12  13309  ixxub  13310  ixxlb  13311  iocssre  13371  icossre  13372  iccssre  13373  icodisj  13420  fzss1  13508  fzss2  13509  ssfzunsnext  13514  fzosplit  13638  fzouzsplit  13640  ssfzo12bi  13707  ssnn0fi  13938  fsuppmapnn0fiub  13944  suppssfz  13947  sswrd  14475  rtrclreclem3  15013  isercoll  15621  summolem2a  15668  fsumcvg3  15682  fsum2dlem  15723  fsumcom2  15727  qshash  15781  prodmolem2a  15890  fprod2dlem  15936  fprodcom2  15940  bitsfzo  16395  1arith  16889  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  ramtlecl  16962  prmgaplem3  17015  prmgaplem4  17016  monhom  17693  epihom  17700  funcsetcres2  18051  funcestrcsetclem8  18104  funcsetcestrclem8  18119  psdmrn  18530  chnrss  18572  chndss  18573  gsumwspan  18805  frmdss2  18822  sursubmefmnd  18855  injsubmefmnd  18856  trivsubgsnd  19120  ssnmz  19132  trivnsgd  19138  kerf1ghm  19213  conjnmz  19218  symgvalstruct  19363  gex1  19557  sylow2alem1  19583  lsmless1x  19610  lsmless2x  19611  lsmub1x  19612  lsmub2x  19613  lsmmod  19641  lsmdisj2  19648  efgrelexlemb  19716  efgcpbllemb  19721  cntzcmn  19806  gsum2d2  19940  dprdub  19993  dprdss  19997  dprddisj2  20007  pgpfac1lem3  20045  subrngmre  20530  subrguss  20555  subrgmre  20565  rnghmsscmap2  20597  rnghmsscmap  20598  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap2  20626  rhmsscmap  20627  rhmsscrnghm  20633  rngcresringcat  20637  funcringcsetc  20642  unitrrg  20671  isdrng2  20711  primefld0cl  20774  primefld1cl  20775  lssssr  20940  lsssssubg  20944  lssmre  20952  lbspss  21069  lspdisj  21115  lbsextlem2  21149  lidl1el  21216  drngnidl  21233  lpiss  21319  zsssubrg  21415  qsssubdrg  21416  cnsubrg  21417  mulgrhm2  21468  znrrg  21555  ocvocv  21661  ocv2ss  21663  ocvin  21664  lsmcss  21682  cssmre  21683  pjcss  21706  lindfrn  21811  sraassab  21858  mhpsubg  22129  evls1maprnss  22353  dmatsgrp  22474  scmatsgrp  22494  scmatsgrp1  22497  m2cpmrngiso  22733  bastg  22941  tgss  22943  tgtop  22948  tgidm  22955  en2top  22960  neisspw  23082  topssnei  23099  neiptopuni  23105  lpss3  23119  clslp  23123  tgrest  23134  ssrest  23151  restntr  23157  ordtbas2  23166  ordtbas  23167  cnss1  23251  cnss2  23252  cnsscnp  23254  cnrest2r  23262  cmpsublem  23374  cmpsub  23375  tgcmp  23376  cmpcld  23377  hauscmplem  23381  cnconn  23397  llyss  23454  nllyss  23455  restnlly  23457  restlly  23458  locfincmp  23501  locfincf  23506  kgenss  23518  kgenidm  23522  llycmpkgen2  23525  1stckgen  23529  kgen2ss  23530  kgencn3  23533  ptbasfi  23556  ptpjopn  23587  txdis  23607  txkgen  23627  xkoptsub  23629  xkopjcn  23631  txconn  23664  qtoptop2  23674  qtopuni  23677  qtopkgen  23685  basqtop  23686  tgqtop  23687  qtopss  23690  qtoprest  23692  qtopomap  23693  qtopcmap  23694  kqsat  23706  kqcldsat  23708  hmphdis  23771  isfild  23833  ssfg  23847  fgss  23848  fgss2  23849  fgfil  23850  fgabs  23854  filconn  23858  fgtr  23865  uzrest  23872  ufilmax  23882  ufileu  23894  filufint  23895  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  flimss2  23947  flimss1  23948  flimclsi  23953  flimcf  23957  flimsncls  23961  fclssscls  23993  fclsss1  23997  fclsss2  23998  fclscf  24000  uffclsflim  24006  alexsublem  24019  alexsubALTlem3  24024  ptcmplem2  24028  ptcmplem3  24029  cnextf  24041  efmndtmd  24076  symgtgp  24081  cldsubg  24086  tsmscl  24110  haustsms2  24112  tgptsmscls  24125  tsmsxp  24130  restutop  24212  ustuqtop4  24219  utop2nei  24225  utop3cls  24226  ucncn  24259  xblss2ps  24376  xblss2  24377  xrsblre  24787  xrsmopn  24788  recld2  24790  zdis  24792  icccmplem2  24799  cncfss  24876  cnheiborlem  24931  htpycn  24950  phtpyhtpy  24959  pi1blem  25016  cphsscph  25228  cfilfcls  25251  iscmet3lem2  25269  iscmet2  25271  caussi  25274  equivcfil  25276  lmcau  25290  metsscmetcld  25292  hlhil  25420  ivthicc  25435  ovoliunnul  25484  ovolicopnf  25501  uniioombllem3  25562  dyadmbllem  25576  volsup2  25582  vitalilem2  25586  itg1addlem4  25676  itg10a  25687  itg1ge0a  25688  mbfi1fseqlem4  25695  itg2gt0  25737  limciun  25871  perfdvf  25880  cpnord  25912  dvcj  25927  dvlip2  25972  dvivth  25987  dvne0  25988  dvcnvre  25996  ply1lpir  26157  plyco0  26167  plyexmo  26290  abelth  26419  efif1o  26523  logno1  26613  efopnlem2  26634  loglesqrt  26738  lgamcvg2  27032  ppisval  27081  ppinprm  27129  chtnprm  27131  fsumvma  27190  dchrfi  27232  chtppilimlem2  27451  chebbnd2  27454  vmadivsumb  27460  rplogsumlem2  27462  dchrisumlem2  27467  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  selbergb  27526  selberg2b  27529  selberg3lem1  27534  selberg3lem2  27535  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  oldssmade  27873  ltslpss  27914  noseqrdgfn  28312  n0ssoldg  28359  peano5uzs  28410  uhgredgss  29214  usgruspgrb  29266  uhgrissubgr  29358  uhgrspansubgrlem  29373  uhgrspan1  29386  cusgredg  29507  usgredgsscusgredg  29543  ococss  31379  shsub1  31410  shless  31445  shmodsi  31475  pjhth  31479  spansnss  31657  spanpr  31666  spansnm0i  31736  pjjsi  31786  sumdmdii  32501  sumdmdlem  32504  sumdmdlem2  32505  cdj3lem1  32520  abrexss  32597  fnpreimac  32758  rnmposs  32761  uzssico  32872  ssnnssfz  32875  pwrssmgc  33075  pmtrcnel  33165  cycpmrn  33219  cyc3evpm  33226  cycpmgcl  33229  elrgspnlem1  33318  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem2  33324  fldgensdrg  33390  ringlsmss1  33471  ringlsmss2  33472  prmidlssidl  33520  mxidlirredi  33546  drngmxidl  33552  drngmxidlr  33553  1arithidomlem1  33610  1arithidom  33612  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  ply1mulrtss  33657  esplyfvaln  33733  dimkerim  33787  extdg1id  33826  irngss  33847  irngssv  33848  algextdeglem8  33884  constrsscn  33900  constrsslem  33901  constrsdrg  33935  crefss  34009  cmpcref  34010  zarmxt1  34040  tpr2rico  34072  esumrnmpt2  34228  esumpcvgval  34238  ldsysgenld  34320  sigapildsys  34322  ldgenpisys  34326  cldssbrsiga  34347  measdivcstALTV  34385  mbfmcnt  34428  oddpwdc  34514  eulerpartlemgs2  34540  reprpmtf1o  34786  bnj1033  35127  bnj1398  35192  trssfir1om  35271  r1omhfb  35272  trssfir1omregs  35296  r1omhfbregs  35297  sconnpi1  35437  cvmscld  35471  cvmliftlem15  35496  satfrnmapom  35568  dfon2lem6  35984  fnessref  36555  fgmin  36568  tailfb  36575  dissneqlem  37670  icoreresf  37682  rdglimss  37707  finxpreclem6  37726  lindsenlbs  37950  poimirlem11  37966  poimirlem12  37967  sstotbnd3  38111  prdstotbnd  38129  cntotbnd  38131  ismtyhmeo  38140  1idl  38361  disjdmqsss  39240  lshpdisj  39447  lssats  39472  lkrin  39624  glbconxN  39838  paddss1  40277  paddss2  40278  paddasslem16  40295  paddidm  40301  pmodlem2  40307  pmapjoin  40312  pmapjat1  40313  pclfinN  40360  pclfinclN  40410  diasslssN  41519  dia2dimlem12  41535  dihsslss  41736  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  zndvdchrrhm  42426  dvrelog2  42517  dvrelog3  42518  aks4d1p3  42531  aks4d1p4  42532  aks4d1p5  42533  aks4d1p7  42536  aks4d1p8  42540  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  hashscontpow1  42574  aks6d1c4  42577  sticksstones3  42601  aks6d1c6lem3  42625  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  rhmqusspan  42638  unitscyglem1  42648  unitscyglem4  42651  eldiophss  43220  rencldnfilem  43266  pellexlem5  43279  pell14qrss1234  43302  pell1qrss14  43314  pellfundre  43327  pellfundge  43328  pellfundlb  43330  pellfundglb  43331  harinf  43480  proot1hash  43641  safesnsupfiss  43860  intabssd  43964  ss2iundf  44104  ov2ssiunov2  44145  clsk1indlem3  44488  radcnvrat  44759  nznngen  44761  trsspwALT3  45264  sspwimpALT2  45372  refsumcn  45479  iinssf  45586  icoiccdif  45972  icccncfext  46333  stoweidlem27  46473  stoweidlem46  46492  stoweidlem57  46503  fourierdlem40  46593  fourierdlem78  46630  ffnafv  47631  iccpartrn  47902  sprsymrelfvlem  47962  sprsymrelf1lem  47963  clnbgrssedg  48329  stgrusgra  48447  rhmsubcALTVlem4  48772  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  ssnn0ssfz  48837  lincolss  48922  lcoss  48924  lcosslsp  48926  iunord  50163