Theorem ssriv 3926

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890

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

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

This theorem is referenced by:  ssid  3945  ssv  3947  ssrab2  4021  difss  4077  ssun1  4119  inss1  4178  0ss  4341  difprsnss  4743  snsspw  4788  uniin  4875  pwuni  4889  iuniin  4947  iunpwss  5050  relopabi  5771  dmin  5860  dmrnssfld  5923  dmcoss  5924  dmcossOLD  5925  dminss  6111  imainss  6112  fvssunirn  6865  fviss  6911  opabresex2  7414  fvmptopab  7415  mapfoss  8792  fsetsspwxp  8793  mapsspm  8817  pmsspw  8818  uniixp  8862  pwfilem  9221  dffi3  9337  dfom3  9559  onwf  9745  tcrank  9799  djuss  9835  djuunxp  9836  djuun  9841  cardprclem  9894  alephsson  10013  ackbij1  10150  cardcf  10165  cfeq0  10169  dfacfin7  10312  hsmexlem6  10344  canthnum  10563  inaprc  10750  nqerf  10844  addnqf  10862  mulnqf  10863  dmrecnq  10882  reclem2pr  10962  wuncn  11084  zssre  12522  zsscn  12523  nnssz  12537  elq  12891  zssq  12897  qssre  12900  ixxssixx  13303  iooval2  13322  ioossre  13351  rge0ssre  13400  fzssz  13471  fz1ssnn  13500  fzssuz  13510  fzssp1  13512  uzdisj  13542  fz0ssnn0  13567  nn0disj  13589  fzossfz  13624  fzouzsplit  13640  fzo0ssnn0  13692  uzrdgfni  13911  seqcoll  14417  wrdexb  14478  fclim  15506  isercolllem3  15620  climcnds  15807  divcnv  15809  harmonic  15815  bitsss  16386  prmssnn  16636  prmssuz2  16657  maxprmfct  16670  1arith  16889  4sqlem19  16925  vdwlem12  16954  restsspw  17385  mremre  17557  mreacs  17615  isfunc  17822  homarel  17994  ledm  18547  lern  18548  chnexg  18575  smndex1basss  18867  sgrpssmgm  18895  mndsssgrp  18896  prdsgrpd  19017  prdsinvgd  19018  symgpssefmnd  19362  symgsubmefmndALT  19369  pgrpsubgsymg  19375  symgtrf  19435  odf1o2  19539  sylow3lem3  19595  sylow3lem6  19598  oppglsm  19608  efgsfo  19705  0frgp  19745  prdscmnd  19827  prdsabld  19828  dprdssv  19984  dprdres  19996  prdsrngd  20148  ringssrng  20258  prdsringd  20291  prdscrngd  20292  unitss  20347  subrngint  20528  subrgint  20563  srhmsubc  20648  subdrgint  20771  sdrgint  20772  primefld  20773  lssintcl  20950  prdslmodd  20955  cnsubmlem  21404  cnsubglem  21405  cnsubdrglem  21408  cnmsubglem  21420  xrge0subm  21433  zringunit  21456  zringlpir  21457  znf1o  21541  ocvss  21660  dsmmsubg  21733  dsmmlss  21734  lbslinds  21823  unitg  22942  cldss2  23005  indiscld  23066  iscldtop  23070  llyssnlly  23453  llyidm  23463  nllyidm  23464  toplly  23465  hauslly  23467  lly1stc  23471  dissnref  23503  txindis  23609  pthaus  23613  ptcmpfi  23788  ufinffr  23904  cnflf2  23978  flimfcls  24001  alexsubALTlem3  24024  ptcmplem1  24027  ptcmpg  24032  prdstmdd  24099  prdstgpd  24100  ust0  24195  prdsms  24506  qdensere  24744  blssioo  24770  tgioo  24771  xrtgioo  24782  xrsmopn  24788  zdis  24792  reperflem  24794  xrge0gsumle  24809  xrge0tsms  24810  icopnfhmeo  24920  bndth  24935  voliunlem2  25528  voliunlem3  25529  vitali  25590  ismbf3d  25631  itg2seq  25719  limccl  25852  limcresi  25862  dvef  25957  aasscn  26295  qssaa  26301  aannenlem2  26306  aannenlem3  26307  ulmcn  26377  mtestbdd  26383  iblulm  26385  reeff1o  26425  reefgim  26428  efifo  26524  dfrelog  26542  relogf1o  26543  logdmss  26619  logcn  26624  dvloglem  26625  logf1o2  26627  dvlog  26628  dvlog2lem  26629  dvlog2  26630  logtayl  26637  cxpcn  26722  cxpcn2  26723  cxpcn3  26725  resqrtcn  26726  efrlim  26946  efrlimOLD  26947  dfef2  26948  cxp2lim  26954  basellem3  27060  basellem4  27061  sqff1o  27159  dchrmhm  27218  chtppilim  27452  chto1lb  27455  chpchtlim  27456  chpo1ub  27457  dchrisumlema  27465  selberg2lem  27527  selberg3lem2  27535  pntrsumo1  27542  pnt2  27590  pnt  27591  madef  27842  oniso  28277  bdayn0sf1o  28376  dfnns2  28378  axcontlem2  29048  usgrexmplef  29342  griedg0ssusgr  29348  nbgrssvtx  29425  nbgrssovtx  29444  uvtxssvtx  29473  rgrusgrprc  29673  clwlkswks  29859  wwlkssswrd  29945  wwlkssswwlksn  29949  wspthsswwlkn  30001  wspthsswwlknon  30004  clwwlksclwwlkn  30116  phrel  30901  bnrel  30953  hlrel  30976  shex  31298  chsssh  31311  hhssnv  31350  choc1  31413  shunssi  31454  shsleji  31456  shsub1i  31458  shsub2i  31459  shsidmi  31470  omlsii  31489  spanuni  31630  spansni  31643  5oalem7  31746  3oalem3  31750  pjrni  31788  mayete3i  31814  hmopex  31961  cnlnssadj  32166  adjbdln  32169  adjsslnop  32173  shatomistici  32447  hatomistici  32448  xrge0tsmsd  33149  primefldchr  33377  1fldgenq  33398  zringidom  33626  esumpcvgval  34238  hashf2  34244  insiga  34297  sigapisys  34315  sigaldsys  34319  sigapildsys  34322  sxbrsigalem0  34431  dya2icobrsiga  34436  sxbrsigalem1  34445  sxbrsigalem2  34446  eulerpartlemb  34528  chtvalz  34789  logdivsqrle  34810  bnj1398  35192  bnj1498  35219  r1omfi  35264  fineqvacALT  35277  erdszelem9  35397  erdsze2lem2  35402  kur14lem9  35412  ptpconn  35431  iinllyconn  35452  cvmlift3  35526  mppsthm  35777  imagesset  36151  altxpsspw  36175  topjoin  36563  onsstopbas  36627  onsucconni  36635  onintopssconn  36638  onint1  36647  oninhaus  36648  ttcid  36690  dfttc4lem2  36727  dfttc4  36728  bj-snglss  37293  bj-imdirco  37520  bj-modssabl  37610  bj-rvecssmod  37626  bj-rvecssvec  37631  bj-rvecsscmod  37633  icoreunrn  37689  difunieq  37704  poimirlem8  37963  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem31  37986  poimirlem32  37987  heiborlem3  38148  disjsssrels  39271  atssbase  39750  readvrec2  42807  eldioph3b  43211  diophin  43218  diophun  43219  eldiophss  43220  isnumbasabl  43552  isnumbasgrp  43553  dfacbasgrp  43554  mon1psubm  43645  omssrncard  43985  inintabss  44023  intimass  44099  inaex  44742  nzin  44763  unipwrVD  45276  unipwr  45277  supxrre3  45773  fsumiunss  46023  rrpsscn  46036  dvnmul  46389  dvnprodlem2  46393  stoweidlem34  46480  stirlinglem13  46532  fourierdlem20  46573  fourierdlem62  46614  fourierdlem83  46635  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fouriersw  46677  qndenserrnbllem  46740  sge0iunmptlemre  46861  nn0ssge0  46870  sge0isum  46873  sge0seq  46892  sge0reuz  46893  caragendifcl  46960  carageniuncllem2  46968  hoicvrrex  47002  smfaddlem1  47209  smfaddlem2  47210  mbfpsssmf  47229  clnbgrssvtx  48319  srhmsubcALTV  48813  lvecpsslmod  48995  thincssc  49911  aacllem  50288  amgmwlem  50289  amgmlemALT  50290