Theorem ssrdv 3937

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

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

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 1943

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

This theorem is used by:  eqelssd  3952  ss2abim  4008  ss2abdv  4013  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  eq0rdvALT  4366  sspw  4568  elpwdifsn  4752  uniss  4875  intss1  4923  intmin  4928  intssuni  4930  iinssiun  4965  iunss1  4966  iinss1  4967  ss2iun  4970  ssiun  5005  ssiun2  5006  iinss  5015  iinss2  5016  iunxdif3  5055  sspwb  5417  pwssun  5543  relop  5828  dmss  5884  dmcosseq  5960  dmcosseqOLD  5961  ssrnres  6170  sossfld  6178  imadifssranOLD  6201  imadifssranOLDOLD  6202  predtrss  6324  preddowncl  6334  tron  6384  tz7.7  6387  funimassd  6949  dffv2  6978  chfnrn  7046  fvn0ssdmfun  7072  fveqdmss  7076  dff3  7098  ffnfv  7117  f1imass  7266  ssorduni  7791  onint  7802  limsssuc  7859  limuni3  7861  limomss  7880  fo1stres  8025  fo2ndres  8026  fo2ndf  8130  fnse  8143  ressuppssdif  8195  suppss  8204  reldmtpos  8244  fprlem2  8312  onfununi  8342  smoiun  8362  smocdmdom  8369  tz7.48-1  8446  tz7.49  8448  oaass  8562  cofon1  8674  cofon2  8675  qsss  8789  uniinqs  8811  pmss12g  8890  mapss  8910  ixpssmap2g  8948  ixpssmapg  8949  pssnn  9177  fineqv  9251  unifi3  9344  finnzfsuppd  9358  ssfii  9404  dffi2  9408  oismo  9527  unxpwdom2  9575  inf3lemd  9621  inf3lem1  9622  inf3lem6  9627  cantnflem3  9685  cantnf  9687  cnfcom3lem  9697  onssr1  9836  rankunb  9857  tcrank  9894  elhf3OLD  9916  harcard  10052  carduni  10055  infxpenlem  10085  infpwfien  10134  dfac12r  10218  ackbij2lem1  10289  ackbij1lem18  10307  isfin1-3  10457  fin1a2lem11  10481  fin1a2lem13  10483  zorn2lem4  10570  zorn2lem5  10571  ttukeylem6  10585  ttukeylem7  10586  fpwwe2lem10  10718  fpwwe2lem11  10719  fpwwe2  10721  wunr1om  10797  wunom  10798  tskr1om  10845  tskhf  10846  tskxpss  10850  tskcard  10859  tskuni  10861  grothomex  10907  genpss  11082  distrlem1pr  11103  distrlem5pr  11105  ltexprlem2  11115  ltexprlem6  11119  ltexprlem7  11120  reclem3pr  11127  reclem4pr  11128  supaddc  12277  supadd  12278  supmul1  12279  supmullem2  12281  peano5uzi  12781  uzss  12981  ixxdisj  13484  ixxss1  13487  ixxss2  13488  ixxss12  13489  ixxub  13490  ixxlb  13491  iocssre  13551  icossre  13552  iccssre  13553  icodisj  13600  fzss1  13690  fzss2  13691  ssfzunsnext  13696  fzosplit  13820  fzouzsplit  13822  ssfzo12bi  13889  ssnn0fi  14121  fsuppmapnn0fiub  14127  suppssfz  14130  sswrd  14660  rtrclreclem3  15206  isercoll  15828  summolem2a  15874  fsumcvg3  15888  fsum2dlem  15929  fsumcom2  15933  qshash  15987  prodmolem2a  16094  fprod2dlem  16140  fprodcom2  16144  bitsfzo  16598  1arith  17098  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  ramtlecl  17171  prmgaplem3  17224  prmgaplem4  17225  monhom  17903  epihom  17910  funcsetcres2  18261  funcestrcsetclem8  18314  funcsetcestrclem8  18329  psdmrn  18740  chnrss  18782  chndss  18783  gsumwspan  19035  frmdss2  19052  sursubmefmnd  19085  injsubmefmnd  19086  trivsubgsnd  19357  ssnmz  19369  trivnsgd  19375  kerf1ghm  19454  conjnmz  19459  symgvalstruct  19604  gex1  19798  sylow2alem1  19824  lsmless1x  19851  lsmless2x  19852  lsmub1x  19853  lsmub2x  19854  lsmmod  19882  lsmdisj2  19889  efgrelexlemb  19957  efgcpbllemb  19962  cntzcmn  20047  gsum2d2  20181  dprdub  20234  dprdss  20238  dprddisj2  20248  pgpfac1lem3  20286  subrngmre  20807  subrguss  20832  subrgmre  20842  rnghmsscmap2  20874  rnghmsscmap  20875  funcrngcsetc  20885  funcrngcsetcALT  20886  rhmsscmap2  20903  rhmsscmap  20904  rhmsscrnghm  20910  rngcresringcat  20914  funcringcsetc  20919  unitrrg  20948  isdrng2  20990  primefld0cl  21056  primefld1cl  21057  lssssr  21222  lsssssubg  21226  lssmre  21234  lbspss  21350  lspdisj  21396  lbsextlem2  21430  lidl1el  21498  drngnidl  21524  prmidlssidl  21619  lpiss  21646  zsssubrg  21724  qsssubdrg  21725  cnsubrg  21726  mulgrhm2  21777  znrrg  21864  ocvocv  21970  ocv2ss  21972  ocvin  21973  lsmcss  21991  cssmre  21992  pjcss  22015  lindfrn  22120  lindsenlbs  22150  sraassab  22169  mhpsubg  22467  evls1maprnss  22689  dmatsgrp  22807  scmatsgrp  22827  scmatsgrp1  22830  m2cpmrngiso  23069  bastg  23277  tgss  23279  tgtop  23284  tgidm  23291  en2top  23296  neisspw  23418  topssnei  23435  neiptopuni  23441  lpss3  23455  clslp  23459  tgrest  23470  ssrest  23487  restntr  23493  ordtbas2  23502  ordtbas  23503  cnss1  23587  cnss2  23588  cnsscnp  23590  cnrest2r  23598  cmpsublem  23710  cmpsub  23711  tgcmp  23712  cmpcld  23713  hauscmplem  23717  cnconn  23733  llyss  23791  nllyss  23792  restnlly  23794  restlly  23795  locfincmp  23838  locfincf  23843  kgenss  23855  kgenidm  23859  llycmpkgen2  23862  1stckgen  23866  kgen2ss  23867  kgencn3  23870  ptbasfi  23893  ptpjopn  23924  txdis  23944  txkgen  23964  xkoptsub  23966  xkopjcn  23968  txconn  24001  qtoptop2  24011  qtopuni  24014  qtopkgen  24022  basqtop  24023  tgqtop  24024  qtopss  24027  qtoprest  24029  qtopomap  24030  qtopcmap  24031  kqsat  24043  kqcldsat  24045  hmphdis  24108  isfild  24170  ssfg  24184  fgss  24185  fgss2  24186  fgfil  24187  fgabs  24191  filconn  24195  fgtr  24202  uzrest  24209  ufilmax  24219  ufileu  24231  filufint  24232  rnelfm  24265  fmfnfmlem2  24267  fmfnfmlem4  24269  flimss2  24284  flimss1  24285  flimclsi  24290  flimcf  24294  flimsncls  24298  fclssscls  24330  fclsss1  24334  fclsss2  24335  fclscf  24337  uffclsflim  24343  alexsublem  24356  alexsubALTlem3  24361  ptcmplem2  24365  ptcmplem3  24366  cnextf  24378  efmndtmd  24413  symgtgp  24418  cldsubg  24423  tsmscl  24447  haustsms2  24449  tgptsmscls  24462  tsmsxp  24467  restutop  24549  ustuqtop4  24556  utop2nei  24562  utop3cls  24563  ucncn  24596  xblss2ps  24713  xblss2  24714  xrsblre  25124  xrsmopn  25125  recld2  25127  zdis  25129  icccmplem2  25136  cncfss  25213  cnheiborlem  25268  htpycn  25287  phtpyhtpy  25296  pi1blem  25353  cphsscph  25565  cfilfcls  25588  iscmet3lem2  25606  iscmet2  25608  caussi  25611  equivcfil  25613  lmcau  25627  metsscmetcld  25629  hlhil  25757  ivthicc  25772  ovoliunnul  25821  ovolicopnf  25838  uniioombllem3  25899  dyadmbllem  25913  volsup2  25919  vitalilem2  25923  itg1addlem4  26013  itg10a  26024  itg1ge0a  26025  mbfi1fseqlem4  26032  itg2gt0  26074  limciun  26207  perfdvf  26216  cpnord  26248  dvcj  26263  dvlip2  26308  dvivth  26323  dvne0  26324  dvcnvre  26332  ply1lpir  26493  plyco0  26503  plyconz  26624  plyexmo  26629  abelth  26761  efif1o  26867  logno1  26957  efopnlem2  26978  loglesqrt  27082  lgamcvg2  27375  ppisval  27424  ppinprm  27472  chtnprm  27474  fsumvma  27533  dchrfi  27575  chtppilimlem2  27794  chebbnd2  27797  vmadivsumb  27803  rplogsumlem2  27805  dchrisumlem2  27810  vmalogdivsum2  27858  vmalogdivsum  27859  2vmadivsumlem  27860  selbergb  27869  selberg2b  27872  selberg3lem1  27877  selberg3lem2  27878  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrlog2bndlem2  27898  pntrlog2bndlem4  27900  oldssmade  28246  ltslpss  28287  noseqrdgfn  28685  n0ssoldg  28732  peano5uzs  28783  elplnglnid  29254  lnincplng  29255  plngrotlem2  29259  cgrabasimass  29371  prlngpln3  29420  uhgredgss  29702  usgruspgrb  29757  uhgrissubgr  29849  uhgrspansubgrlem  29864  uhgrspan1  29877  cusgredg  29998  usgredgsscusgredg  30033  ococss  31888  shsub1  31919  shless  31954  shmodsi  31984  pjhth  31988  spansnss  32166  spanpr  32175  spansnm0i  32245  pjjsi  32295  sumdmdii  33010  sumdmdlem  33013  sumdmdlem2  33014  cdj3lem1  33029  abrexss  33101  fnpreimac  33257  rnmposs  33260  uzssico  33369  ssnnssfz  33372  pwrssmgc  33554  pmtrcnel  33643  cycpmrn  33697  cyc3evpm  33704  cycpmgcl  33707  elrgspnlem1  33796  elrgspnlem3  33798  elrgspnlem4  33799  elrgspnsubrunlem2  33802  fldgensdrg  33869  ringlsmss1  33942  ringlsmss2  33943  mxidlirredi  33989  drngmxidl  33994  drngmxidlr  33995  1arithidomlem1  34060  1arithidom  34062  1arithufdlem2  34070  1arithufdlem3  34071  1arithufdlem4  34072  dfufd2lem  34074  ply1mulrtss  34107  esplyfvaln  34199  dimkerim  34252  extdg1id  34291  irngss  34312  irngssv  34313  algextdeglem8  34349  constrsscn  34365  constrsslem  34366  constrsdrg  34400  crefss  34474  cmpcref  34475  zarmxt1  34505  tpr2rico  34537  esumrnmpt2  34693  esumpcvgval  34703  ldsysgenld  34786  sigapildsys  34788  ldgenpisys  34792  cldssbrsiga  34813  measdivcstALTV  34851  mbfmcnt  34893  oddpwdc  34979  eulerpartlemgs2  35005  reprpmtf1o  35248  bnj1033  35592  bnj1398  35657  trssfir1om  35726  r1omhfb  35727  trssfir1omregs  35787  r1omhfbregs  35788  sconnpi1  35983  cvmscld  36017  cvmliftlem15  36042  satfrnmapom  36114  dfon2lem6  36530  fnessref  37125  fgmin  37138  tailfb  37145  dissneqlem  38243  icoreresf  38255  rdglimss  38280  finxpreclem6  38299  poimirlem11  38529  poimirlem12  38530  sstotbnd3  38690  prdstotbnd  38708  cntotbnd  38710  ismtyhmeo  38719  1idl  38940  disjdmqsss  39817  lshpdisj  40024  lssats  40049  lkrin  40201  glbconxN  40415  paddss1  40854  paddss2  40855  paddasslem16  40872  paddidm  40878  pmodlem2  40884  pmapjoin  40889  pmapjat1  40890  pclfinN  40937  pclfinclN  40987  diasslssN  42096  dia2dimlem12  42112  dihsslss  42313  baerlem3lem2  42747  baerlem5alem2  42748  baerlem5blem2  42749  zndvdchrrhm  43003  dvrelog2  43094  dvrelog3  43095  aks4d1p3  43108  aks4d1p4  43109  aks4d1p5  43110  aks4d1p7  43113  aks4d1p8  43117  primrootsunit1  43127  primrootscoprmpow  43129  primrootscoprbij  43132  hashscontpow1  43151  aks6d1c4  43154  sticksstones3  43178  aks6d1c6lem3  43202  aks6d1c6isolem2  43205  aks6d1c6lem5  43207  rhmqusspan  43215  unitscyglem1  43225  unitscyglem4  43228  eldiophss  43764  rencldnfilem  43806  pellexlem5  43819  pell14qrss1234  43842  pell1qrss14  43854  pellfundre  43867  pellfundge  43868  pellfundlb  43870  pellfundglb  43871  harinf  44020  proot1hash  44181  safesnsupfiss  44400  intabssd  44504  ss2iundf  44644  ov2ssiunov2  44685  clsk1indlem3  45028  radcnvrat  45283  nznngen  45285  trsspwALT3  45787  sspwimpALT2  45895  refsumcn  46016  iinssf  46122  icoiccdif  46505  icccncfext  46866  stoweidlem27  47006  stoweidlem46  47025  stoweidlem57  47036  fourierdlem40  47126  fourierdlem78  47163  ffnafv  48210  iccpartrn  48481  sprsymrelfvlem  48541  sprsymrelf1lem  48542  clnbgrssedg  48908  stgrusgra  49026  rhmsubcALTVlem4  49350  funcringcsetcALTV2lem8  49363  funcringcsetclem8ALTV  49386  ssnn0ssfz  49430  lincolss  49515  lcoss  49517  lcosslsp  49519  iunord  50753