Theorem ssriv 3998

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962

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

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

This theorem is referenced by:  ssid  4017  ssv  4019  ssrab2  4089  difss  4145  ssun1  4187  inss1  4244  0ss  4405  difprsnss  4803  snsspw  4848  uniin  4935  pwuni  4949  iuniin  5008  iunpwss  5111  relopabi  5834  dmin  5924  dmrnssfld  5986  dmcoss  5987  dminss  6174  imainss  6175  fvssunirn  6939  fviss  6985  opabresex2  7484  fvmptopab  7486  mapfoss  8890  fsetsspwxp  8891  mapsspm  8914  pmsspw  8915  uniixp  8959  pwfilem  9353  dffi3  9468  dfom3  9684  onwf  9867  tcrank  9921  djuss  9957  djuunxp  9958  djuun  9963  cardprclem  10016  alephsson  10137  ackbij1  10274  cardcf  10289  cfeq0  10293  dfacfin7  10436  hsmexlem6  10468  canthnum  10686  inaprc  10873  nqerf  10967  addnqf  10985  mulnqf  10986  dmrecnq  11005  reclem2pr  11085  wuncn  11207  zssre  12617  zsscn  12618  nnssz  12632  elq  12989  zssq  12995  qssre  12998  ixxssixx  13397  iooval2  13416  ioossre  13444  rge0ssre  13492  fzssz  13562  fz1ssnn  13591  fzssuz  13601  fzssp1  13603  uzdisj  13633  fz0ssnn0  13658  nn0disj  13680  fzossfz  13714  fzouzsplit  13730  fzo0ssnn0  13781  uzrdgfni  13995  seqcoll  14499  wrdexb  14559  fclim  15585  isercolllem3  15699  climcnds  15883  divcnv  15885  harmonic  15891  bitsss  16459  prmssnn  16709  maxprmfct  16742  1arith  16960  4sqlem19  16996  vdwlem12  17025  restsspw  17477  mremre  17648  mreacs  17702  isfunc  17914  homarel  18089  ledm  18647  lern  18648  smndex1basss  18930  sgrpssmgm  18958  mndsssgrp  18959  prdsgrpd  19080  prdsinvgd  19081  symgpssefmnd  19427  symgsubmefmndALT  19435  pgrpsubgsymg  19441  symgtrf  19501  odf1o2  19605  sylow3lem3  19661  sylow3lem6  19664  oppglsm  19674  efgsfo  19771  0frgp  19811  prdscmnd  19893  prdsabld  19894  dprdssv  20050  dprdres  20062  prdsrngd  20193  ringssrng  20299  prdsringd  20334  prdscrngd  20335  unitss  20392  subrngint  20576  subrgint  20611  srhmsubc  20696  subdrgint  20820  sdrgint  20821  primefld  20822  lssintcl  20979  prdslmodd  20984  xrge0subm  21442  cnsubmlem  21449  cnsubglem  21450  cnsubdrglem  21453  cnmsubglem  21465  zringunit  21494  zringlpir  21495  znf1o  21587  ocvss  21705  dsmmsubg  21780  dsmmlss  21781  lbslinds  21870  unitg  22989  cldss2  23053  indiscld  23114  iscldtop  23118  llyssnlly  23501  llyidm  23511  nllyidm  23512  toplly  23513  hauslly  23515  lly1stc  23519  dissnref  23551  txindis  23657  pthaus  23661  ptcmpfi  23836  ufinffr  23952  cnflf2  24026  flimfcls  24049  alexsubALTlem3  24072  ptcmplem1  24075  ptcmpg  24080  prdstmdd  24147  prdstgpd  24148  ust0  24243  prdsms  24559  qdensere  24805  blssioo  24830  tgioo  24831  xrtgioo  24841  xrsmopn  24847  zdis  24851  reperflem  24853  xrge0gsumle  24868  xrge0tsms  24869  icopnfhmeo  24987  bndth  25003  voliunlem2  25599  voliunlem3  25600  vitali  25661  ismbf3d  25702  itg2seq  25791  limccl  25924  limcresi  25934  dvef  26032  aasscn  26374  qssaa  26380  aannenlem2  26385  aannenlem3  26386  ulmcn  26456  mtestbdd  26462  iblulm  26464  reeff1o  26505  reefgim  26508  efifo  26603  dfrelog  26621  relogf1o  26622  logdmss  26698  logcn  26703  dvloglem  26704  logf1o2  26706  dvlog  26707  dvlog2lem  26708  dvlog2  26709  logtayl  26716  cxpcn  26801  cxpcnOLD  26802  cxpcn2  26803  cxpcn3  26805  resqrtcn  26806  efrlim  27026  efrlimOLD  27027  dfef2  27028  cxp2lim  27034  basellem3  27140  basellem4  27141  sqff1o  27239  dchrmhm  27299  chtppilim  27533  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  dchrisumlema  27546  selberg2lem  27608  selberg3lem2  27616  pntrsumo1  27623  pnt2  27671  pnt  27672  madef  27909  n0ssold  28369  dfnns2  28376  axcontlem2  28994  usgrexmplef  29290  griedg0ssusgr  29296  nbgrssvtx  29373  nbgrssovtx  29392  uvtxssvtx  29421  rgrusgrprc  29621  clwlkswks  29808  wwlkssswrd  29891  wwlkssswwlksn  29895  wspthsswwlkn  29947  wspthsswwlknon  29950  clwwlksclwwlkn  30059  phrel  30843  bnrel  30895  hlrel  30918  shex  31240  chsssh  31253  hhssnv  31292  choc1  31355  shunssi  31396  shsleji  31398  shsub1i  31400  shsub2i  31401  shsidmi  31412  omlsii  31431  spanuni  31572  spansni  31585  5oalem7  31688  3oalem3  31692  pjrni  31730  mayete3i  31756  hmopex  31903  cnlnssadj  32108  adjbdln  32111  adjsslnop  32115  shatomistici  32389  hatomistici  32390  xrge0tsmsd  33047  primefldchr  33282  1fldgenq  33303  zringidom  33558  esumpcvgval  34058  hashf2  34064  insiga  34117  sigapisys  34135  sigaldsys  34139  sigapildsys  34142  sxbrsigalem0  34252  dya2icobrsiga  34257  sxbrsigalem1  34266  sxbrsigalem2  34267  eulerpartlemb  34349  chtvalz  34622  logdivsqrle  34643  bnj1398  35026  bnj1498  35053  fineqvacALT  35090  erdszelem9  35183  erdsze2lem2  35188  kur14lem9  35198  ptpconn  35217  iinllyconn  35238  cvmlift3  35312  mppsthm  35563  imagesset  35934  altxpsspw  35958  topjoin  36347  onsstopbas  36411  onsucconni  36419  onintopssconn  36422  onint1  36431  oninhaus  36432  bj-snglss  36952  bj-imdirco  37172  bj-modssabl  37262  bj-rvecssmod  37278  bj-rvecssvec  37283  bj-rvecsscmod  37285  icoreunrn  37341  difunieq  37356  poimirlem8  37614  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem31  37637  poimirlem32  37638  heiborlem3  37799  atssbase  39271  readvrec2  42369  eldioph3b  42752  diophin  42759  diophun  42760  eldiophss  42761  isnumbasabl  43094  isnumbasgrp  43095  dfacbasgrp  43096  mon1psubm  43187  omssrncard  43529  inintabss  43567  intimass  43643  inaex  44292  nzin  44313  unipwrVD  44829  unipwr  44830  supxrre3  45274  fsumiunss  45530  rrpsscn  45543  dvnmul  45898  dvnprodlem2  45902  stoweidlem34  45989  stirlinglem13  46041  fourierdlem20  46082  fourierdlem62  46123  fourierdlem83  46144  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fouriersw  46186  qndenserrnbllem  46249  sge0iunmptlemre  46370  nn0ssge0  46379  sge0isum  46382  sge0seq  46401  sge0reuz  46402  caragendifcl  46469  carageniuncllem2  46477  hoicvrrex  46511  smfaddlem1  46718  smfaddlem2  46719  mbfpsssmf  46738  upwordsseti  46838  clnbgrssvtx  47755  srhmsubcALTV  48168  lvecpsslmod  48352  thincssc  48825  aacllem  49031  amgmwlem  49032  amgmlemALT  49033