Theorem ssriv 3962

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926

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 3943

This theorem is referenced by:  ssid  3981  ssv  3983  ssrab2  4055  difss  4111  ssun1  4153  inss1  4212  0ss  4375  difprsnss  4775  snsspw  4820  uniin  4907  pwuni  4921  iuniin  4980  iunpwss  5083  relopabi  5801  dmin  5891  dmrnssfld  5953  dmcoss  5954  dminss  6142  imainss  6143  fvssunirn  6908  fviss  6955  opabresex2  7457  fvmptopab  7459  mapfoss  8864  fsetsspwxp  8865  mapsspm  8888  pmsspw  8889  uniixp  8933  pwfilem  9326  dffi3  9441  dfom3  9659  onwf  9842  tcrank  9896  djuss  9932  djuunxp  9933  djuun  9938  cardprclem  9991  alephsson  10112  ackbij1  10249  cardcf  10264  cfeq0  10268  dfacfin7  10411  hsmexlem6  10443  canthnum  10661  inaprc  10848  nqerf  10942  addnqf  10960  mulnqf  10961  dmrecnq  10980  reclem2pr  11060  wuncn  11182  zssre  12593  zsscn  12594  nnssz  12608  elq  12964  zssq  12970  qssre  12973  ixxssixx  13374  iooval2  13393  ioossre  13422  rge0ssre  13471  fzssz  13541  fz1ssnn  13570  fzssuz  13580  fzssp1  13582  uzdisj  13612  fz0ssnn0  13637  nn0disj  13659  fzossfz  13693  fzouzsplit  13709  fzo0ssnn0  13760  uzrdgfni  13974  seqcoll  14480  wrdexb  14541  fclim  15567  isercolllem3  15681  climcnds  15865  divcnv  15867  harmonic  15873  bitsss  16443  prmssnn  16693  maxprmfct  16726  1arith  16945  4sqlem19  16981  vdwlem12  17010  restsspw  17443  mremre  17614  mreacs  17668  isfunc  17875  homarel  18047  ledm  18598  lern  18599  smndex1basss  18881  sgrpssmgm  18909  mndsssgrp  18910  prdsgrpd  19031  prdsinvgd  19032  symgpssefmnd  19375  symgsubmefmndALT  19382  pgrpsubgsymg  19388  symgtrf  19448  odf1o2  19552  sylow3lem3  19608  sylow3lem6  19611  oppglsm  19621  efgsfo  19718  0frgp  19758  prdscmnd  19840  prdsabld  19841  dprdssv  19997  dprdres  20009  prdsrngd  20134  ringssrng  20244  prdsringd  20279  prdscrngd  20280  unitss  20334  subrngint  20518  subrgint  20553  srhmsubc  20638  subdrgint  20761  sdrgint  20762  primefld  20763  lssintcl  20919  prdslmodd  20924  xrge0subm  21373  cnsubmlem  21380  cnsubglem  21381  cnsubdrglem  21384  cnmsubglem  21396  zringunit  21425  zringlpir  21426  znf1o  21510  ocvss  21628  dsmmsubg  21701  dsmmlss  21702  lbslinds  21791  unitg  22903  cldss2  22966  indiscld  23027  iscldtop  23031  llyssnlly  23414  llyidm  23424  nllyidm  23425  toplly  23426  hauslly  23428  lly1stc  23432  dissnref  23464  txindis  23570  pthaus  23574  ptcmpfi  23749  ufinffr  23865  cnflf2  23939  flimfcls  23962  alexsubALTlem3  23985  ptcmplem1  23988  ptcmpg  23993  prdstmdd  24060  prdstgpd  24061  ust0  24156  prdsms  24468  qdensere  24706  blssioo  24732  tgioo  24733  xrtgioo  24744  xrsmopn  24750  zdis  24754  reperflem  24756  xrge0gsumle  24771  xrge0tsms  24772  icopnfhmeo  24890  bndth  24906  voliunlem2  25502  voliunlem3  25503  vitali  25564  ismbf3d  25605  itg2seq  25693  limccl  25826  limcresi  25836  dvef  25934  aasscn  26276  qssaa  26282  aannenlem2  26287  aannenlem3  26288  ulmcn  26358  mtestbdd  26364  iblulm  26366  reeff1o  26407  reefgim  26410  efifo  26506  dfrelog  26524  relogf1o  26525  logdmss  26601  logcn  26606  dvloglem  26607  logf1o2  26609  dvlog  26610  dvlog2lem  26611  dvlog2  26612  logtayl  26619  cxpcn  26704  cxpcnOLD  26705  cxpcn2  26706  cxpcn3  26708  resqrtcn  26709  efrlim  26929  efrlimOLD  26930  dfef2  26931  cxp2lim  26937  basellem3  27043  basellem4  27044  sqff1o  27142  dchrmhm  27202  chtppilim  27436  chto1lb  27439  chpchtlim  27440  chpo1ub  27441  dchrisumlema  27449  selberg2lem  27511  selberg3lem2  27519  pntrsumo1  27526  pnt2  27574  pnt  27575  madef  27812  n0ssold  28272  dfnns2  28279  axcontlem2  28890  usgrexmplef  29184  griedg0ssusgr  29190  nbgrssvtx  29267  nbgrssovtx  29286  uvtxssvtx  29315  rgrusgrprc  29515  clwlkswks  29704  wwlkssswrd  29790  wwlkssswwlksn  29794  wspthsswwlkn  29846  wspthsswwlknon  29849  clwwlksclwwlkn  29958  phrel  30742  bnrel  30794  hlrel  30817  shex  31139  chsssh  31152  hhssnv  31191  choc1  31254  shunssi  31295  shsleji  31297  shsub1i  31299  shsub2i  31300  shsidmi  31311  omlsii  31330  spanuni  31471  spansni  31484  5oalem7  31587  3oalem3  31591  pjrni  31629  mayete3i  31655  hmopex  31802  cnlnssadj  32007  adjbdln  32010  adjsslnop  32014  shatomistici  32288  hatomistici  32289  xrge0tsmsd  33002  primefldchr  33241  1fldgenq  33262  zringidom  33512  esumpcvgval  34055  hashf2  34061  insiga  34114  sigapisys  34132  sigaldsys  34136  sigapildsys  34139  sxbrsigalem0  34249  dya2icobrsiga  34254  sxbrsigalem1  34263  sxbrsigalem2  34264  eulerpartlemb  34346  chtvalz  34607  logdivsqrle  34628  bnj1398  35011  bnj1498  35038  fineqvacALT  35075  erdszelem9  35167  erdsze2lem2  35172  kur14lem9  35182  ptpconn  35201  iinllyconn  35222  cvmlift3  35296  mppsthm  35547  imagesset  35917  altxpsspw  35941  topjoin  36329  onsstopbas  36393  onsucconni  36401  onintopssconn  36404  onint1  36413  oninhaus  36414  bj-snglss  36934  bj-imdirco  37154  bj-modssabl  37244  bj-rvecssmod  37260  bj-rvecssvec  37265  bj-rvecsscmod  37267  icoreunrn  37323  difunieq  37338  poimirlem8  37598  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem31  37621  poimirlem32  37622  heiborlem3  37783  atssbase  39254  readvrec2  42351  eldioph3b  42735  diophin  42742  diophun  42743  eldiophss  42744  isnumbasabl  43077  isnumbasgrp  43078  dfacbasgrp  43079  mon1psubm  43170  omssrncard  43511  inintabss  43549  intimass  43625  inaex  44269  nzin  44290  unipwrVD  44804  unipwr  44805  supxrre3  45300  fsumiunss  45552  rrpsscn  45565  dvnmul  45920  dvnprodlem2  45924  stoweidlem34  46011  stirlinglem13  46063  fourierdlem20  46104  fourierdlem62  46145  fourierdlem83  46166  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fouriersw  46208  qndenserrnbllem  46271  sge0iunmptlemre  46392  nn0ssge0  46401  sge0isum  46404  sge0seq  46423  sge0reuz  46424  caragendifcl  46491  carageniuncllem2  46499  hoicvrrex  46533  smfaddlem1  46740  smfaddlem2  46741  mbfpsssmf  46760  upwordsseti  46862  clnbgrssvtx  47793  srhmsubcALTV  48248  lvecpsslmod  48431  thincssc  49258  aacllem  49613  amgmwlem  49614  amgmlemALT  49615