Theorem ssriv 3980

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3944

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

This theorem depends on definitions:  df-bi 206  df-ss 3961

This theorem is referenced by:  ssid  3999  ssv  4001  ssrab2  4073  difss  4128  ssun1  4170  inss1  4227  0ss  4398  difprsnss  4804  snsspw  4847  uniin  4935  pwuni  4949  iuniin  5009  iunpwss  5111  relopabi  5824  dmin  5914  dmrnssfld  5973  dmcoss  5974  dminss  6159  imainss  6160  fvssunirn  6929  fviss  6974  opabresex2  7472  fvmptopab  7474  mapfoss  8871  fsetsspwxp  8872  mapsspm  8895  pmsspw  8896  uniixp  8940  pwfilem  9202  pwfilemOLD  9372  dffi3  9456  dfom3  9672  onwf  9855  tcrank  9909  djuss  9945  djuunxp  9946  djuun  9951  cardprclem  10004  alephsson  10125  ackbij1  10263  cardcf  10277  cfeq0  10281  dfacfin7  10424  hsmexlem6  10456  canthnum  10674  inaprc  10861  nqerf  10955  addnqf  10973  mulnqf  10974  dmrecnq  10993  reclem2pr  11073  wuncn  11195  zssre  12598  zsscn  12599  nnssz  12613  elq  12967  zssq  12973  qssre  12976  ixxssixx  13373  iooval2  13392  ioossre  13420  rge0ssre  13468  fzssz  13538  fz1ssnn  13567  fzssuz  13577  fzssp1  13579  uzdisj  13609  fz0ssnn0  13631  nn0disj  13652  fzossfz  13686  fzouzsplit  13702  fzo0ssnn0  13748  uzrdgfni  13959  seqcoll  14461  wrdexb  14511  fclim  15533  isercolllem3  15649  climcnds  15833  divcnv  15835  harmonic  15841  bitsss  16404  prmssnn  16650  maxprmfct  16683  1arith  16899  4sqlem19  16935  vdwlem12  16964  restsspw  17416  mremre  17587  mreacs  17641  isfunc  17853  homarel  18028  ledm  18585  lern  18586  smndex1basss  18865  sgrpssmgm  18893  mndsssgrp  18894  prdsgrpd  19014  prdsinvgd  19015  symgpssefmnd  19362  symgsubmefmndALT  19370  pgrpsubgsymg  19376  symgtrf  19436  odf1o2  19540  sylow3lem3  19596  sylow3lem6  19599  oppglsm  19609  efgsfo  19706  0frgp  19746  prdscmnd  19828  prdsabld  19829  dprdssv  19985  dprdres  19997  prdsrngd  20128  ringssrng  20234  prdsringd  20269  prdscrngd  20270  unitss  20327  subrngint  20509  subrgint  20546  srhmsubc  20625  subdrgint  20703  sdrgint  20704  primefld  20705  lssintcl  20860  prdslmodd  20865  xrge0subm  21357  cnsubmlem  21364  cnsubglem  21365  cnsubdrglem  21368  cnmsubglem  21380  zringunit  21409  zringlpir  21410  znf1o  21502  ocvss  21619  dsmmsubg  21694  dsmmlss  21695  lbslinds  21784  unitg  22914  cldss2  22978  indiscld  23039  iscldtop  23043  llyssnlly  23426  llyidm  23436  nllyidm  23437  toplly  23438  hauslly  23440  lly1stc  23444  dissnref  23476  txindis  23582  pthaus  23586  ptcmpfi  23761  ufinffr  23877  cnflf2  23951  flimfcls  23974  alexsubALTlem3  23997  ptcmplem1  24000  ptcmpg  24005  prdstmdd  24072  prdstgpd  24073  ust0  24168  prdsms  24484  qdensere  24730  blssioo  24755  tgioo  24756  xrtgioo  24766  xrsmopn  24772  zdis  24776  reperflem  24778  xrge0gsumle  24793  xrge0tsms  24794  icopnfhmeo  24912  bndth  24928  voliunlem2  25524  voliunlem3  25525  vitali  25586  ismbf3d  25627  itg2seq  25716  limccl  25848  limcresi  25858  dvef  25956  aasscn  26298  qssaa  26304  aannenlem2  26309  aannenlem3  26310  ulmcn  26380  mtestbdd  26386  iblulm  26388  reeff1o  26429  reefgim  26432  efifo  26526  dfrelog  26544  relogf1o  26545  logdmss  26621  logcn  26626  dvloglem  26627  logf1o2  26629  dvlog  26630  dvlog2lem  26631  dvlog2  26632  logtayl  26639  cxpcn  26724  cxpcnOLD  26725  cxpcn2  26726  cxpcn3  26728  resqrtcn  26729  efrlim  26946  efrlimOLD  26947  dfef2  26948  cxp2lim  26954  basellem3  27060  basellem4  27061  sqff1o  27159  dchrmhm  27219  chtppilim  27453  chto1lb  27456  chpchtlim  27457  chpo1ub  27458  dchrisumlema  27466  selberg2lem  27528  selberg3lem2  27536  pntrsumo1  27543  pnt2  27591  pnt  27592  madef  27829  n0ssold  28270  axcontlem2  28848  usgrexmplef  29144  griedg0ssusgr  29150  nbgrssvtx  29227  nbgrssovtx  29246  uvtxssvtx  29275  rgrusgrprc  29475  clwlkswks  29662  wwlkssswrd  29745  wwlkssswwlksn  29749  wspthsswwlkn  29801  wspthsswwlknon  29804  clwwlksclwwlkn  29913  phrel  30697  bnrel  30749  hlrel  30772  shex  31094  chsssh  31107  hhssnv  31146  choc1  31209  shunssi  31250  shsleji  31252  shsub1i  31254  shsub2i  31255  shsidmi  31266  omlsii  31285  spanuni  31426  spansni  31439  5oalem7  31542  3oalem3  31546  pjrni  31584  mayete3i  31610  hmopex  31757  cnlnssadj  31962  adjbdln  31965  adjsslnop  31969  shatomistici  32243  hatomistici  32244  xrge0tsmsd  32861  primefldchr  33087  1fldgenq  33108  zringidom  33366  esumpcvgval  33828  hashf2  33834  insiga  33887  sigapisys  33905  sigaldsys  33909  sigapildsys  33912  sxbrsigalem0  34022  dya2icobrsiga  34027  sxbrsigalem1  34036  sxbrsigalem2  34037  eulerpartlemb  34119  chtvalz  34392  logdivsqrle  34413  bnj1398  34796  bnj1498  34823  fineqvacALT  34849  erdszelem9  34940  erdsze2lem2  34945  kur14lem9  34955  ptpconn  34974  iinllyconn  34995  cvmlift3  35069  mppsthm  35320  imagesset  35680  altxpsspw  35704  topjoin  35980  onsstopbas  36044  onsucconni  36052  onintopssconn  36055  onint1  36064  oninhaus  36065  bj-snglss  36580  bj-imdirco  36800  bj-modssabl  36890  bj-rvecssmod  36906  bj-rvecssvec  36911  bj-rvecsscmod  36913  icoreunrn  36969  difunieq  36984  poimirlem8  37232  poimirlem18  37242  poimirlem21  37245  poimirlem22  37246  poimirlem31  37255  poimirlem32  37256  heiborlem3  37417  atssbase  38892  eldioph3b  42327  diophin  42334  diophun  42335  eldiophss  42336  isnumbasabl  42672  isnumbasgrp  42673  dfacbasgrp  42674  mon1psubm  42769  omssrncard  43112  inintabss  43150  intimass  43226  inaex  43876  nzin  43897  unipwrVD  44413  unipwr  44414  supxrre3  44845  fsumiunss  45101  rrpsscn  45114  dvnmul  45469  dvnprodlem2  45473  stoweidlem34  45560  stirlinglem13  45612  fourierdlem20  45653  fourierdlem62  45694  fourierdlem83  45715  fourierdlem101  45733  fourierdlem103  45735  fourierdlem104  45736  fourierdlem111  45743  fouriersw  45757  qndenserrnbllem  45820  sge0iunmptlemre  45941  nn0ssge0  45950  sge0isum  45953  sge0seq  45972  sge0reuz  45973  caragendifcl  46040  carageniuncllem2  46048  hoicvrrex  46082  smfaddlem1  46289  smfaddlem2  46290  mbfpsssmf  46309  upwordsseti  46409  clnbgrssvtx  47307  srhmsubcALTV  47573  lvecpsslmod  47761  thincssc  48218  aacllem  48420  amgmwlem  48421  amgmlemALT  48422