Theorem ssrdv 3931

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2109   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  eqelssd  3946  ss2abdvALT  4002  sscon  4077  ssdif  4078  unss1  4117  ssrin  4172  eq0rdvALT  4344  sspw  4551  elpwdifsn  4727  uniss  4852  intss1  4899  intmin  4904  intssuni  4906  iinssiun  4942  iunss1  4943  iinss1  4944  ss2iun  4947  ssiun  4980  ssiun2  4981  iinss  4990  iinss2  4991  iunxdif3  5028  sspwb  5367  pwssun  5484  relop  5756  dmss  5808  dmcosseq  5879  ssrnres  6078  sossfld  6086  predtrss  6222  preddowncl  6232  tron  6286  tz7.7  6289  dffv2  6857  chfnrn  6920  fvn0ssdmfun  6946  fveqdmss  6950  dff3  6970  ffnfv  6986  f1imass  7131  ssorduni  7619  onint  7630  limsssuc  7685  limuni3  7687  limomss  7705  fo1stres  7843  fo2ndres  7844  fo2ndf  7946  fnse  7958  ressuppssdif  7985  suppss  7994  suppssOLD  7995  reldmtpos  8034  fprlem2  8101  onfununi  8156  smoiun  8176  smorndom  8183  tz7.48-1  8258  tz7.49  8260  oaass  8368  qsss  8541  uniinqs  8560  pmss12g  8631  mapss  8651  ixpssmap2g  8689  ixpssmapg  8690  pssnn  8916  fineqv  8999  pssnnOLD  9001  ssfii  9139  dffi2  9143  oismo  9260  unxpwdom2  9308  inf3lemd  9346  inf3lem1  9347  inf3lem6  9352  cantnflem3  9410  cantnf  9412  cnfcom3lem  9422  onssr1  9573  rankunb  9592  tcrank  9626  harcard  9720  carduni  9723  infxpenlem  9753  infpwfien  9802  dfac12r  9886  ackbij2lem1  9959  ackbij1lem18  9977  isfin1-3  10126  fin1a2lem11  10150  fin1a2lem13  10152  zorn2lem4  10239  zorn2lem5  10240  ttukeylem6  10254  ttukeylem7  10255  fpwwe2lem10  10380  fpwwe2lem11  10381  fpwwe2  10383  wunr1om  10459  wunom  10460  tskr1om  10507  tskr1om2  10508  tskxpss  10512  tskcard  10521  tskuni  10523  grothomex  10569  genpss  10744  distrlem1pr  10765  distrlem5pr  10767  ltexprlem2  10777  ltexprlem6  10781  ltexprlem7  10782  reclem3pr  10789  reclem4pr  10790  supaddc  11925  supadd  11926  supmul1  11927  supmullem2  11929  peano5uzi  12392  uzss  12587  ixxdisj  13076  ixxss1  13079  ixxss2  13080  ixxss12  13081  ixxub  13082  ixxlb  13083  iocssre  13141  icossre  13142  iccssre  13143  icodisj  13190  fzss1  13277  fzss2  13278  ssfzunsnext  13283  fzosplit  13401  fzouzsplit  13403  ssfzo12bi  13463  ssnn0fi  13686  fsuppmapnn0fiub  13692  suppssfz  13695  sswrd  14206  rtrclreclem3  14752  isercoll  15360  summolem2a  15408  fsumcvg3  15422  fsum2dlem  15463  fsumcom2  15467  qshash  15520  prodmolem2a  15625  fprod2dlem  15671  fprodcom2  15675  bitsfzo  16123  1arith  16609  vdwlem2  16664  vdwlem6  16668  vdwlem8  16670  ramtlecl  16682  prmgaplem3  16735  prmgaplem4  16736  monhom  17428  epihom  17435  funcsetcres2  17789  funcestrcsetclem8  17845  funcsetcestrclem8  17860  psdmrn  18272  gsumwspan  18466  frmdss2  18483  sursubmefmnd  18516  injsubmefmnd  18517  trivsubgsnd  18763  ssnmz  18775  trivnsgd  18781  conjnmz  18849  symgvalstruct  18985  symgvalstructOLD  18986  gex1  19177  sylow2alem1  19203  lsmless1x  19230  lsmless2x  19231  lsmub1x  19232  lsmub2x  19233  lsmmod  19262  lsmdisj2  19269  efgrelexlemb  19337  efgcpbllemb  19342  cntzcmn  19422  gsum2d2  19556  dprdub  19609  dprdss  19613  dprddisj2  19623  pgpfac1lem3  19661  kerf1ghm  19968  isdrng2  19982  subrguss  20020  subrgmre  20029  primefld0cl  20055  primefld1cl  20056  lssssr  20196  lsssssubg  20201  lssmre  20209  lbspss  20325  lspdisj  20368  lbsextlem2  20402  lidl1el  20470  drngnidl  20481  lpiss  20502  unitrrg  20545  zsssubrg  20637  qsssubdrg  20638  cnsubrg  20639  mulgrhm2  20681  znrrg  20754  ocvocv  20857  ocv2ss  20859  ocvin  20860  lsmcss  20878  cssmre  20879  pjcss  20904  lindfrn  21009  mhpsubg  21324  dmatsgrp  21629  scmatsgrp  21649  scmatsgrp1  21652  m2cpmrngiso  21888  bastg  22097  tgss  22099  tgtop  22104  tgidm  22111  en2top  22116  neisspw  22239  topssnei  22256  neiptopuni  22262  lpss3  22276  clslp  22280  tgrest  22291  ssrest  22308  restntr  22314  ordtbas2  22323  ordtbas  22324  cnss1  22408  cnss2  22409  cnsscnp  22411  cnrest2r  22419  cmpsublem  22531  cmpsub  22532  tgcmp  22533  cmpcld  22534  hauscmplem  22538  cnconn  22554  llyss  22611  nllyss  22612  restnlly  22614  restlly  22615  locfincmp  22658  locfincf  22663  kgenss  22675  kgenidm  22679  llycmpkgen2  22682  1stckgen  22686  kgen2ss  22687  kgencn3  22690  ptbasfi  22713  ptpjopn  22744  txdis  22764  txkgen  22784  xkoptsub  22786  xkopjcn  22788  txconn  22821  qtoptop2  22831  qtopuni  22834  qtopkgen  22842  basqtop  22843  tgqtop  22844  qtopss  22847  qtoprest  22849  qtopomap  22850  qtopcmap  22851  kqsat  22863  kqcldsat  22865  hmphdis  22928  isfild  22990  ssfg  23004  fgss  23005  fgss2  23006  fgfil  23007  fgabs  23011  filconn  23015  fgtr  23022  uzrest  23029  ufilmax  23039  ufileu  23051  filufint  23052  rnelfm  23085  fmfnfmlem2  23087  fmfnfmlem4  23089  flimss2  23104  flimss1  23105  flimclsi  23110  flimcf  23114  flimsncls  23118  fclssscls  23150  fclsss1  23154  fclsss2  23155  fclscf  23157  uffclsflim  23163  alexsublem  23176  alexsubALTlem3  23181  ptcmplem2  23185  ptcmplem3  23186  cnextf  23198  efmndtmd  23233  symgtgp  23238  cldsubg  23243  tsmscl  23267  haustsms2  23269  tgptsmscls  23282  tsmsxp  23287  restutop  23370  ustuqtop4  23377  utop2nei  23383  utop3cls  23384  ucncn  23418  xblss2ps  23535  xblss2  23536  xrsblre  23955  xrsmopn  23956  recld2  23958  zdis  23960  icccmplem2  23967  cncfss  24043  cnheiborlem  24098  htpycn  24117  phtpyhtpy  24126  pi1blem  24183  cphsscph  24396  cfilfcls  24419  iscmet3lem2  24437  iscmet2  24439  caussi  24442  equivcfil  24444  lmcau  24458  metsscmetcld  24460  hlhil  24588  ivthicc  24603  ovoliunnul  24652  ovolicopnf  24669  uniioombllem3  24730  dyadmbllem  24744  volsup2  24750  vitalilem2  24754  itg1addlem4  24844  itg1addlem4OLD  24845  itg10a  24856  itg1ge0a  24857  mbfi1fseqlem4  24864  itg2gt0  24906  limciun  25039  perfdvf  25048  cpnord  25080  dvcj  25095  dvlip2  25140  dvivth  25155  dvne0  25156  dvcnvre  25164  ply1lpir  25324  plyco0  25334  plyexmo  25454  abelth  25581  efif1o  25683  logno1  25772  efopnlem2  25793  loglesqrt  25892  lgamcvg2  26185  ppisval  26234  ppinprm  26282  chtnprm  26284  fsumvma  26342  dchrfi  26384  chtppilimlem2  26603  chebbnd2  26606  vmadivsumb  26612  rplogsumlem2  26614  dchrisumlem2  26619  vmalogdivsum2  26667  vmalogdivsum  26668  2vmadivsumlem  26669  selbergb  26678  selberg2b  26681  selberg3lem1  26686  selberg3lem2  26687  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrlog2bndlem2  26707  pntrlog2bndlem4  26709  uhgredgss  27482  usgruspgrb  27532  uhgrissubgr  27623  uhgrspansubgrlem  27638  uhgrspan1  27651  cusgredg  27772  usgredgsscusgredg  27807  ococss  29634  shsub1  29665  shless  29700  shmodsi  29730  pjhth  29734  spansnss  29912  spanpr  29921  spansnm0i  29991  pjjsi  30041  sumdmdii  30756  sumdmdlem  30759  sumdmdlem2  30760  cdj3lem1  30775  abrexss  30836  fnpreimac  30987  rnmposs  30990  unifi3  31026  uzssico  31084  ssnnssfz  31087  pwrssmgc  31257  pmtrcnel  31337  cycpmrn  31389  cyc3evpm  31396  cycpmgcl  31399  ringlsmss1  31563  ringlsmss2  31564  prmidlssidl  31599  dimkerim  31687  extdg1id  31717  crefss  31778  cmpcref  31779  zarmxt1  31809  tpr2rico  31841  esumrnmpt2  32015  esumpcvgval  32025  ldsysgenld  32107  sigapildsys  32109  ldgenpisys  32113  cldssbrsiga  32134  measdivcstALTV  32172  mbfmcnt  32214  oddpwdc  32300  eulerpartlemgs2  32326  reprpmtf1o  32585  bnj1033  32928  bnj1398  32993  sconnpi1  33180  cvmscld  33214  cvmliftlem15  33239  satfrnmapom  33311  dfon2lem6  33743  oldssmade  34039  sltlpss  34066  fnessref  34525  fgmin  34538  tailfb  34545  dissneqlem  35490  icoreresf  35502  rdglimss  35527  finxpreclem6  35546  lindsenlbs  35751  poimirlem11  35767  poimirlem12  35768  sstotbnd3  35913  prdstotbnd  35931  cntotbnd  35933  ismtyhmeo  35942  1idl  36163  lshpdisj  36980  lssats  37005  lkrin  37157  glbconxN  37371  paddss1  37810  paddss2  37811  paddasslem16  37828  paddidm  37834  pmodlem2  37840  pmapjoin  37845  pmapjat1  37846  pclfinN  37893  pclfinclN  37943  diasslssN  39052  dia2dimlem12  39068  dihsslss  39269  baerlem3lem2  39703  baerlem5alem2  39704  baerlem5blem2  39705  dvrelog2  40052  dvrelog3  40053  aks4d1p3  40066  aks4d1p4  40067  aks4d1p5  40068  aks4d1p7  40071  aks4d1p8  40075  sticksstones3  40084  eldiophss  40576  rencldnfilem  40622  pellexlem5  40635  pell14qrss1234  40658  pell1qrss14  40670  pellfundre  40683  pellfundge  40684  pellfundlb  40686  pellfundglb  40687  harinf  40836  proot1hash  41005  intabssd  41088  ss2iundf  41220  ov2ssiunov2  41261  clsk1indlem3  41606  finnzfsuppd  41773  radcnvrat  41885  nznngen  41887  trsspwALT3  42393  sspwimpALT2  42501  refsumcn  42526  iinssf  42640  icoiccdif  43016  icccncfext  43382  stoweidlem27  43522  stoweidlem46  43541  stoweidlem57  43552  fourierdlem40  43642  fourierdlem78  43679  ffnafv  44614  iccpartrn  44834  sprsymrelfvlem  44894  sprsymrelf1lem  44895  rnghmsscmap2  45483  rnghmsscmap  45484  funcrngcsetc  45508  funcrngcsetcALT  45509  rhmsscmap2  45529  rhmsscmap  45530  rhmsscrnghm  45536  rngcresringcat  45540  funcringcsetc  45545  funcringcsetcALTV2lem8  45553  funcringcsetclem8ALTV  45576  rhmsubcALTVlem4  45617  ssnn0ssfz  45637  lincolss  45727  lcoss  45729  lcosslsp  45731  iunord  46334