Theorem ssriv 3950

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		df-ss 3931	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1799	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795

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

This theorem is referenced by:  ssid  3969  ssv  3971  ssrab2  4043  difss  4099  ssun1  4141  inss1  4200  0ss  4363  difprsnss  4763  snsspw  4808  uniin  4895  pwuni  4909  iuniin  4968  iunpwss  5071  relopabi  5785  dmin  5875  dmrnssfld  5937  dmcoss  5938  dminss  6126  imainss  6127  fvssunirn  6891  fviss  6938  opabresex2  7441  fvmptopab  7443  mapfoss  8825  fsetsspwxp  8826  mapsspm  8849  pmsspw  8850  uniixp  8894  pwfilem  9267  dffi3  9382  dfom3  9600  onwf  9783  tcrank  9837  djuss  9873  djuunxp  9874  djuun  9879  cardprclem  9932  alephsson  10053  ackbij1  10190  cardcf  10205  cfeq0  10209  dfacfin7  10352  hsmexlem6  10384  canthnum  10602  inaprc  10789  nqerf  10883  addnqf  10901  mulnqf  10902  dmrecnq  10921  reclem2pr  11001  wuncn  11123  zssre  12536  zsscn  12537  nnssz  12551  elq  12909  zssq  12915  qssre  12918  ixxssixx  13320  iooval2  13339  ioossre  13368  rge0ssre  13417  fzssz  13487  fz1ssnn  13516  fzssuz  13526  fzssp1  13528  uzdisj  13558  fz0ssnn0  13583  nn0disj  13605  fzossfz  13639  fzouzsplit  13655  fzo0ssnn0  13707  uzrdgfni  13923  seqcoll  14429  wrdexb  14490  fclim  15519  isercolllem3  15633  climcnds  15817  divcnv  15819  harmonic  15825  bitsss  16396  prmssnn  16646  maxprmfct  16679  1arith  16898  4sqlem19  16934  vdwlem12  16963  restsspw  17394  mremre  17565  mreacs  17619  isfunc  17826  homarel  17998  ledm  18549  lern  18550  smndex1basss  18832  sgrpssmgm  18860  mndsssgrp  18861  prdsgrpd  18982  prdsinvgd  18983  symgpssefmnd  19326  symgsubmefmndALT  19333  pgrpsubgsymg  19339  symgtrf  19399  odf1o2  19503  sylow3lem3  19559  sylow3lem6  19562  oppglsm  19572  efgsfo  19669  0frgp  19709  prdscmnd  19791  prdsabld  19792  dprdssv  19948  dprdres  19960  prdsrngd  20085  ringssrng  20195  prdsringd  20230  prdscrngd  20231  unitss  20285  subrngint  20469  subrgint  20504  srhmsubc  20589  subdrgint  20712  sdrgint  20713  primefld  20714  lssintcl  20870  prdslmodd  20875  xrge0subm  21324  cnsubmlem  21331  cnsubglem  21332  cnsubdrglem  21335  cnmsubglem  21347  zringunit  21376  zringlpir  21377  znf1o  21461  ocvss  21579  dsmmsubg  21652  dsmmlss  21653  lbslinds  21742  unitg  22854  cldss2  22917  indiscld  22978  iscldtop  22982  llyssnlly  23365  llyidm  23375  nllyidm  23376  toplly  23377  hauslly  23379  lly1stc  23383  dissnref  23415  txindis  23521  pthaus  23525  ptcmpfi  23700  ufinffr  23816  cnflf2  23890  flimfcls  23913  alexsubALTlem3  23936  ptcmplem1  23939  ptcmpg  23944  prdstmdd  24011  prdstgpd  24012  ust0  24107  prdsms  24419  qdensere  24657  blssioo  24683  tgioo  24684  xrtgioo  24695  xrsmopn  24701  zdis  24705  reperflem  24707  xrge0gsumle  24722  xrge0tsms  24723  icopnfhmeo  24841  bndth  24857  voliunlem2  25452  voliunlem3  25453  vitali  25514  ismbf3d  25555  itg2seq  25643  limccl  25776  limcresi  25786  dvef  25884  aasscn  26226  qssaa  26232  aannenlem2  26237  aannenlem3  26238  ulmcn  26308  mtestbdd  26314  iblulm  26316  reeff1o  26357  reefgim  26360  efifo  26456  dfrelog  26474  relogf1o  26475  logdmss  26551  logcn  26556  dvloglem  26557  logf1o2  26559  dvlog  26560  dvlog2lem  26561  dvlog2  26562  logtayl  26569  cxpcn  26654  cxpcnOLD  26655  cxpcn2  26656  cxpcn3  26658  resqrtcn  26659  efrlim  26879  efrlimOLD  26880  dfef2  26881  cxp2lim  26887  basellem3  26993  basellem4  26994  sqff1o  27092  dchrmhm  27152  chtppilim  27386  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  dchrisumlema  27399  selberg2lem  27461  selberg3lem2  27469  pntrsumo1  27476  pnt2  27524  pnt  27525  madef  27764  onsiso  28169  n0ssold  28245  bdayn0sf1o  28259  dfnns2  28261  axcontlem2  28892  usgrexmplef  29186  griedg0ssusgr  29192  nbgrssvtx  29269  nbgrssovtx  29288  uvtxssvtx  29317  rgrusgrprc  29517  clwlkswks  29706  wwlkssswrd  29792  wwlkssswwlksn  29796  wspthsswwlkn  29848  wspthsswwlknon  29851  clwwlksclwwlkn  29960  phrel  30744  bnrel  30796  hlrel  30819  shex  31141  chsssh  31154  hhssnv  31193  choc1  31256  shunssi  31297  shsleji  31299  shsub1i  31301  shsub2i  31302  shsidmi  31313  omlsii  31332  spanuni  31473  spansni  31486  5oalem7  31589  3oalem3  31593  pjrni  31631  mayete3i  31657  hmopex  31804  cnlnssadj  32009  adjbdln  32012  adjsslnop  32016  shatomistici  32290  hatomistici  32291  xrge0tsmsd  33002  primefldchr  33251  1fldgenq  33272  zringidom  33522  esumpcvgval  34068  hashf2  34074  insiga  34127  sigapisys  34145  sigaldsys  34149  sigapildsys  34152  sxbrsigalem0  34262  dya2icobrsiga  34267  sxbrsigalem1  34276  sxbrsigalem2  34277  eulerpartlemb  34359  chtvalz  34620  logdivsqrle  34641  bnj1398  35024  bnj1498  35051  fineqvacALT  35088  erdszelem9  35186  erdsze2lem2  35191  kur14lem9  35201  ptpconn  35220  iinllyconn  35241  cvmlift3  35315  mppsthm  35566  imagesset  35941  altxpsspw  35965  topjoin  36353  onsstopbas  36417  onsucconni  36425  onintopssconn  36428  onint1  36437  oninhaus  36438  bj-snglss  36958  bj-imdirco  37178  bj-modssabl  37268  bj-rvecssmod  37284  bj-rvecssvec  37289  bj-rvecsscmod  37291  icoreunrn  37347  difunieq  37362  poimirlem8  37622  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem31  37645  poimirlem32  37646  heiborlem3  37807  atssbase  39283  readvrec2  42349  eldioph3b  42753  diophin  42760  diophun  42761  eldiophss  42762  isnumbasabl  43095  isnumbasgrp  43096  dfacbasgrp  43097  mon1psubm  43188  omssrncard  43529  inintabss  43567  intimass  43643  inaex  44286  nzin  44307  unipwrVD  44821  unipwr  44822  supxrre3  45321  fsumiunss  45573  rrpsscn  45586  dvnmul  45941  dvnprodlem2  45945  stoweidlem34  46032  stirlinglem13  46084  fourierdlem20  46125  fourierdlem62  46166  fourierdlem83  46187  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fouriersw  46229  qndenserrnbllem  46292  sge0iunmptlemre  46413  nn0ssge0  46422  sge0isum  46425  sge0seq  46444  sge0reuz  46445  caragendifcl  46512  carageniuncllem2  46520  hoicvrrex  46554  smfaddlem1  46761  smfaddlem2  46762  mbfpsssmf  46781  upwordsseti  46883  clnbgrssvtx  47832  srhmsubcALTV  48313  lvecpsslmod  48496  thincssc  49413  aacllem  49790  amgmwlem  49791  amgmlemALT  49792