Theorem ssriv 3951

Description: Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
ssriv.1	⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
ssriv	⊢ 𝐴 ⊆ 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 3933	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1801	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ssid  3969  ssv  3971  ssrab2  4042  difss  4096  ssun1  4137  inss1  4193  0ss  4361  difprsnss  4764  snsspw  4807  uniin  4897  pwuni  4911  iuniin  4971  iunpwss  5072  relopabi  5783  dmin  5872  dmrnssfld  5930  dmcoss  5931  dminss  6110  imainss  6111  fvssunirn  6880  fviss  6923  opabresex2  7414  fvmptopab  7416  mapfoss  8797  fsetsspwxp  8798  mapsspm  8821  pmsspw  8822  uniixp  8866  pwfilem  9128  pwfilemOLD  9297  dffi3  9376  dfom3  9592  onwf  9775  tcrank  9829  djuss  9865  djuunxp  9866  djuun  9871  cardprclem  9924  alephsson  10045  ackbij1  10183  cardcf  10197  cfeq0  10201  dfacfin7  10344  hsmexlem6  10376  canthnum  10594  inaprc  10781  nqerf  10875  addnqf  10893  mulnqf  10894  dmrecnq  10913  reclem2pr  10993  wuncn  11115  zssre  12515  zsscn  12516  nnssz  12530  elq  12884  zssq  12890  qssre  12893  ixxssixx  13288  iooval2  13307  ioossre  13335  rge0ssre  13383  fzssz  13453  fz1ssnn  13482  fzssuz  13492  fzssp1  13494  uzdisj  13524  fz0ssnn0  13546  nn0disj  13567  fzossfz  13601  fzouzsplit  13617  fzo0ssnn0  13663  uzrdgfni  13873  seqcoll  14375  wrdexb  14425  fclim  15447  isercolllem3  15563  climcnds  15747  divcnv  15749  harmonic  15755  bitsss  16317  prmssnn  16563  maxprmfct  16596  1arith  16810  4sqlem19  16846  vdwlem12  16875  restsspw  17327  mremre  17498  mreacs  17552  isfunc  17764  homarel  17936  ledm  18493  lern  18494  smndex1basss  18729  sgrpssmgm  18757  mndsssgrp  18758  prdsgrpd  18871  prdsinvgd  18872  symgpssefmnd  19191  symgsubmefmndALT  19199  pgrpsubgsymg  19205  symgtrf  19265  odf1o2  19369  sylow3lem3  19425  sylow3lem6  19428  oppglsm  19438  efgsfo  19535  0frgp  19575  prdscmnd  19653  prdsabld  19654  dprdssv  19809  dprdres  19821  prdsringd  20050  prdscrngd  20051  unitss  20103  subrgint  20293  subdrgint  20326  sdrgint  20327  primefld  20328  lssintcl  20482  prdslmodd  20487  xrge0subm  20875  cnsubmlem  20882  cnsubglem  20883  cnsubdrglem  20885  cnmsubglem  20897  zringunit  20924  zringlpir  20925  znf1o  20995  ocvss  21111  dsmmsubg  21186  dsmmlss  21187  lbslinds  21276  unitg  22354  cldss2  22418  indiscld  22479  iscldtop  22483  llyssnlly  22866  llyidm  22876  nllyidm  22877  toplly  22878  hauslly  22880  lly1stc  22884  dissnref  22916  txindis  23022  pthaus  23026  ptcmpfi  23201  ufinffr  23317  cnflf2  23391  flimfcls  23414  alexsubALTlem3  23437  ptcmplem1  23440  ptcmpg  23445  prdstmdd  23512  prdstgpd  23513  ust0  23608  prdsms  23924  qdensere  24170  blssioo  24195  tgioo  24196  xrtgioo  24206  xrsmopn  24212  zdis  24216  reperflem  24218  xrge0gsumle  24233  xrge0tsms  24234  icopnfhmeo  24343  bndth  24358  voliunlem2  24952  voliunlem3  24953  vitali  25014  ismbf3d  25055  itg2seq  25144  limccl  25276  limcresi  25286  dvef  25381  aasscn  25715  qssaa  25721  aannenlem2  25726  aannenlem3  25727  ulmcn  25795  mtestbdd  25801  iblulm  25803  reeff1o  25843  reefgim  25846  efifo  25940  dfrelog  25958  relogf1o  25959  logdmss  26034  logcn  26039  dvloglem  26040  logf1o2  26042  dvlog  26043  dvlog2lem  26044  dvlog2  26045  logtayl  26052  cxpcn  26135  cxpcn2  26136  cxpcn3  26138  resqrtcn  26139  efrlim  26356  dfef2  26357  cxp2lim  26363  basellem3  26469  basellem4  26470  sqff1o  26568  dchrmhm  26626  chtppilim  26860  chto1lb  26863  chpchtlim  26864  chpo1ub  26865  dchrisumlema  26873  selberg2lem  26935  selberg3lem2  26943  pntrsumo1  26950  pnt2  26998  pnt  26999  madef  27229  axcontlem2  27977  usgrexmplef  28270  griedg0ssusgr  28276  nbgrssvtx  28353  nbgrssovtx  28372  uvtxssvtx  28401  rgrusgrprc  28600  clwlkswks  28787  wwlkssswrd  28870  wwlkssswwlksn  28874  wspthsswwlkn  28926  wspthsswwlknon  28929  clwwlksclwwlkn  29038  phrel  29820  bnrel  29872  hlrel  29895  shex  30217  chsssh  30230  hhssnv  30269  choc1  30332  shunssi  30373  shsleji  30375  shsub1i  30377  shsub2i  30378  shsidmi  30389  omlsii  30408  spanuni  30549  spansni  30562  5oalem7  30665  3oalem3  30669  pjrni  30707  mayete3i  30733  hmopex  30880  cnlnssadj  31085  adjbdln  31088  adjsslnop  31092  shatomistici  31366  hatomistici  31367  xrge0tsmsd  31969  primefldchr  32147  1fldgenq  32160  esumpcvgval  32766  hashf2  32772  insiga  32825  sigapisys  32843  sigaldsys  32847  sigapildsys  32850  sxbrsigalem0  32960  dya2icobrsiga  32965  sxbrsigalem1  32974  sxbrsigalem2  32975  eulerpartlemb  33057  chtvalz  33331  logdivsqrle  33352  bnj1398  33735  bnj1498  33762  fineqvacALT  33788  erdszelem9  33880  erdsze2lem2  33885  kur14lem9  33895  ptpconn  33914  iinllyconn  33935  cvmlift3  34009  mppsthm  34260  imagesset  34614  altxpsspw  34638  topjoin  34913  onsstopbas  34977  onsucconni  34985  onintopssconn  34988  onint1  34997  oninhaus  34998  bj-snglss  35514  bj-imdirco  35734  bj-modssabl  35824  bj-rvecssmod  35840  bj-rvecssvec  35845  bj-rvecsscmod  35847  icoreunrn  35903  difunieq  35918  poimirlem8  36159  poimirlem18  36169  poimirlem21  36172  poimirlem22  36173  poimirlem31  36182  poimirlem32  36183  heiborlem3  36345  atssbase  37825  eldioph3b  41146  diophin  41153  diophun  41154  eldiophss  41155  isnumbasabl  41491  isnumbasgrp  41492  dfacbasgrp  41493  mon1psubm  41591  omssrncard  41934  inintabss  41972  intimass  42048  inaex  42699  nzin  42720  unipwrVD  43236  unipwr  43237  supxrre3  43680  fsumiunss  43936  rrpsscn  43949  dvnmul  44304  dvnprodlem2  44308  stoweidlem34  44395  stirlinglem13  44447  fourierdlem20  44488  fourierdlem62  44529  fourierdlem83  44550  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  fourierdlem111  44578  fouriersw  44592  qndenserrnbllem  44655  sge0iunmptlemre  44776  nn0ssge0  44785  sge0isum  44788  sge0seq  44807  sge0reuz  44808  caragendifcl  44875  carageniuncllem2  44883  hoicvrrex  44917  smfaddlem1  45124  smfaddlem2  45125  mbfpsssmf  45144  upwordsseti  45244  ringssrng  46298  srhmsubc  46494  srhmsubcALTV  46512  lvecpsslmod  46708  thincssc  47166  aacllem  47368  amgmwlem  47369  amgmlemALT  47370