Theorem ssriv 3953

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

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

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 3934

This theorem is referenced by:  ssid  3972  ssv  3974  ssrab2  4046  difss  4102  ssun1  4144  inss1  4203  0ss  4366  difprsnss  4766  snsspw  4811  uniin  4898  pwuni  4912  iuniin  4971  iunpwss  5074  relopabi  5788  dmin  5878  dmrnssfld  5940  dmcoss  5941  dminss  6129  imainss  6130  fvssunirn  6894  fviss  6941  opabresex2  7444  fvmptopab  7446  mapfoss  8828  fsetsspwxp  8829  mapsspm  8852  pmsspw  8853  uniixp  8897  pwfilem  9274  dffi3  9389  dfom3  9607  onwf  9790  tcrank  9844  djuss  9880  djuunxp  9881  djuun  9886  cardprclem  9939  alephsson  10060  ackbij1  10197  cardcf  10212  cfeq0  10216  dfacfin7  10359  hsmexlem6  10391  canthnum  10609  inaprc  10796  nqerf  10890  addnqf  10908  mulnqf  10909  dmrecnq  10928  reclem2pr  11008  wuncn  11130  zssre  12543  zsscn  12544  nnssz  12558  elq  12916  zssq  12922  qssre  12925  ixxssixx  13327  iooval2  13346  ioossre  13375  rge0ssre  13424  fzssz  13494  fz1ssnn  13523  fzssuz  13533  fzssp1  13535  uzdisj  13565  fz0ssnn0  13590  nn0disj  13612  fzossfz  13646  fzouzsplit  13662  fzo0ssnn0  13714  uzrdgfni  13930  seqcoll  14436  wrdexb  14497  fclim  15526  isercolllem3  15640  climcnds  15824  divcnv  15826  harmonic  15832  bitsss  16403  prmssnn  16653  maxprmfct  16686  1arith  16905  4sqlem19  16941  vdwlem12  16970  restsspw  17401  mremre  17572  mreacs  17626  isfunc  17833  homarel  18005  ledm  18556  lern  18557  smndex1basss  18839  sgrpssmgm  18867  mndsssgrp  18868  prdsgrpd  18989  prdsinvgd  18990  symgpssefmnd  19333  symgsubmefmndALT  19340  pgrpsubgsymg  19346  symgtrf  19406  odf1o2  19510  sylow3lem3  19566  sylow3lem6  19569  oppglsm  19579  efgsfo  19676  0frgp  19716  prdscmnd  19798  prdsabld  19799  dprdssv  19955  dprdres  19967  prdsrngd  20092  ringssrng  20202  prdsringd  20237  prdscrngd  20238  unitss  20292  subrngint  20476  subrgint  20511  srhmsubc  20596  subdrgint  20719  sdrgint  20720  primefld  20721  lssintcl  20877  prdslmodd  20882  xrge0subm  21331  cnsubmlem  21338  cnsubglem  21339  cnsubdrglem  21342  cnmsubglem  21354  zringunit  21383  zringlpir  21384  znf1o  21468  ocvss  21586  dsmmsubg  21659  dsmmlss  21660  lbslinds  21749  unitg  22861  cldss2  22924  indiscld  22985  iscldtop  22989  llyssnlly  23372  llyidm  23382  nllyidm  23383  toplly  23384  hauslly  23386  lly1stc  23390  dissnref  23422  txindis  23528  pthaus  23532  ptcmpfi  23707  ufinffr  23823  cnflf2  23897  flimfcls  23920  alexsubALTlem3  23943  ptcmplem1  23946  ptcmpg  23951  prdstmdd  24018  prdstgpd  24019  ust0  24114  prdsms  24426  qdensere  24664  blssioo  24690  tgioo  24691  xrtgioo  24702  xrsmopn  24708  zdis  24712  reperflem  24714  xrge0gsumle  24729  xrge0tsms  24730  icopnfhmeo  24848  bndth  24864  voliunlem2  25459  voliunlem3  25460  vitali  25521  ismbf3d  25562  itg2seq  25650  limccl  25783  limcresi  25793  dvef  25891  aasscn  26233  qssaa  26239  aannenlem2  26244  aannenlem3  26245  ulmcn  26315  mtestbdd  26321  iblulm  26323  reeff1o  26364  reefgim  26367  efifo  26463  dfrelog  26481  relogf1o  26482  logdmss  26558  logcn  26563  dvloglem  26564  logf1o2  26566  dvlog  26567  dvlog2lem  26568  dvlog2  26569  logtayl  26576  cxpcn  26661  cxpcnOLD  26662  cxpcn2  26663  cxpcn3  26665  resqrtcn  26666  efrlim  26886  efrlimOLD  26887  dfef2  26888  cxp2lim  26894  basellem3  27000  basellem4  27001  sqff1o  27099  dchrmhm  27159  chtppilim  27393  chto1lb  27396  chpchtlim  27397  chpo1ub  27398  dchrisumlema  27406  selberg2lem  27468  selberg3lem2  27476  pntrsumo1  27483  pnt2  27531  pnt  27532  madef  27771  onsiso  28176  n0ssold  28252  bdayn0sf1o  28266  dfnns2  28268  axcontlem2  28899  usgrexmplef  29193  griedg0ssusgr  29199  nbgrssvtx  29276  nbgrssovtx  29295  uvtxssvtx  29324  rgrusgrprc  29524  clwlkswks  29713  wwlkssswrd  29799  wwlkssswwlksn  29803  wspthsswwlkn  29855  wspthsswwlknon  29858  clwwlksclwwlkn  29967  phrel  30751  bnrel  30803  hlrel  30826  shex  31148  chsssh  31161  hhssnv  31200  choc1  31263  shunssi  31304  shsleji  31306  shsub1i  31308  shsub2i  31309  shsidmi  31320  omlsii  31339  spanuni  31480  spansni  31493  5oalem7  31596  3oalem3  31600  pjrni  31638  mayete3i  31664  hmopex  31811  cnlnssadj  32016  adjbdln  32019  adjsslnop  32023  shatomistici  32297  hatomistici  32298  xrge0tsmsd  33009  primefldchr  33258  1fldgenq  33279  zringidom  33529  esumpcvgval  34075  hashf2  34081  insiga  34134  sigapisys  34152  sigaldsys  34156  sigapildsys  34159  sxbrsigalem0  34269  dya2icobrsiga  34274  sxbrsigalem1  34283  sxbrsigalem2  34284  eulerpartlemb  34366  chtvalz  34627  logdivsqrle  34648  bnj1398  35031  bnj1498  35058  fineqvacALT  35095  erdszelem9  35193  erdsze2lem2  35198  kur14lem9  35208  ptpconn  35227  iinllyconn  35248  cvmlift3  35322  mppsthm  35573  imagesset  35948  altxpsspw  35972  topjoin  36360  onsstopbas  36424  onsucconni  36432  onintopssconn  36435  onint1  36444  oninhaus  36445  bj-snglss  36965  bj-imdirco  37185  bj-modssabl  37275  bj-rvecssmod  37291  bj-rvecssvec  37296  bj-rvecsscmod  37298  icoreunrn  37354  difunieq  37369  poimirlem8  37629  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem31  37652  poimirlem32  37653  heiborlem3  37814  atssbase  39290  readvrec2  42356  eldioph3b  42760  diophin  42767  diophun  42768  eldiophss  42769  isnumbasabl  43102  isnumbasgrp  43103  dfacbasgrp  43104  mon1psubm  43195  omssrncard  43536  inintabss  43574  intimass  43650  inaex  44293  nzin  44314  unipwrVD  44828  unipwr  44829  supxrre3  45328  fsumiunss  45580  rrpsscn  45593  dvnmul  45948  dvnprodlem2  45952  stoweidlem34  46039  stirlinglem13  46091  fourierdlem20  46132  fourierdlem62  46173  fourierdlem83  46194  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fouriersw  46236  qndenserrnbllem  46299  sge0iunmptlemre  46420  nn0ssge0  46429  sge0isum  46432  sge0seq  46451  sge0reuz  46452  caragendifcl  46519  carageniuncllem2  46527  hoicvrrex  46561  smfaddlem1  46768  smfaddlem2  46769  mbfpsssmf  46788  upwordsseti  46890  clnbgrssvtx  47836  srhmsubcALTV  48317  lvecpsslmod  48500  thincssc  49417  aacllem  49794  amgmwlem  49795  amgmlemALT  49796