Theorem ssriv 3925

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

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

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 3906

This theorem is referenced by:  ssid  3944  ssv  3946  ssrab2  4020  difss  4076  ssun1  4118  inss1  4177  0ss  4340  difprsnss  4744  snsspw  4787  uniin  4874  pwuni  4888  iuniin  4946  iunpwss  5049  relopabi  5778  dmin  5866  dmrnssfld  5929  dmcoss  5930  dmcossOLD  5931  dminss  6117  imainss  6118  fvssunirn  6871  fviss  6917  opabresex2  7421  fvmptopab  7422  mapfoss  8799  fsetsspwxp  8800  mapsspm  8824  pmsspw  8825  uniixp  8869  pwfilem  9228  dffi3  9344  dfom3  9568  onwf  9754  tcrank  9808  djuss  9844  djuunxp  9845  djuun  9850  cardprclem  9903  alephsson  10022  ackbij1  10159  cardcf  10174  cfeq0  10178  dfacfin7  10321  hsmexlem6  10353  canthnum  10572  inaprc  10759  nqerf  10853  addnqf  10871  mulnqf  10872  dmrecnq  10891  reclem2pr  10971  wuncn  11093  zssre  12531  zsscn  12532  nnssz  12546  elq  12900  zssq  12906  qssre  12909  ixxssixx  13312  iooval2  13331  ioossre  13360  rge0ssre  13409  fzssz  13480  fz1ssnn  13509  fzssuz  13519  fzssp1  13521  uzdisj  13551  fz0ssnn0  13576  nn0disj  13598  fzossfz  13633  fzouzsplit  13649  fzo0ssnn0  13701  uzrdgfni  13920  seqcoll  14426  wrdexb  14487  fclim  15515  isercolllem3  15629  climcnds  15816  divcnv  15818  harmonic  15824  bitsss  16395  prmssnn  16645  prmssuz2  16666  maxprmfct  16679  1arith  16898  4sqlem19  16934  vdwlem12  16963  restsspw  17394  mremre  17566  mreacs  17624  isfunc  17831  homarel  18003  ledm  18556  lern  18557  chnexg  18584  smndex1basss  18876  sgrpssmgm  18904  mndsssgrp  18905  prdsgrpd  19026  prdsinvgd  19027  symgpssefmnd  19371  symgsubmefmndALT  19378  pgrpsubgsymg  19384  symgtrf  19444  odf1o2  19548  sylow3lem3  19604  sylow3lem6  19607  oppglsm  19617  efgsfo  19714  0frgp  19754  prdscmnd  19836  prdsabld  19837  dprdssv  19993  dprdres  20005  prdsrngd  20157  ringssrng  20267  prdsringd  20300  prdscrngd  20301  unitss  20356  subrngint  20537  subrgint  20572  srhmsubc  20657  subdrgint  20780  sdrgint  20781  primefld  20782  lssintcl  20959  prdslmodd  20964  cnsubmlem  21395  cnsubglem  21396  cnsubdrglem  21398  cnmsubglem  21410  xrge0subm  21423  zringunit  21446  zringlpir  21447  znf1o  21531  ocvss  21650  dsmmsubg  21723  dsmmlss  21724  lbslinds  21813  unitg  22932  cldss2  22995  indiscld  23056  iscldtop  23060  llyssnlly  23443  llyidm  23453  nllyidm  23454  toplly  23455  hauslly  23457  lly1stc  23461  dissnref  23493  txindis  23599  pthaus  23603  ptcmpfi  23778  ufinffr  23894  cnflf2  23968  flimfcls  23991  alexsubALTlem3  24014  ptcmplem1  24017  ptcmpg  24022  prdstmdd  24089  prdstgpd  24090  ust0  24185  prdsms  24496  qdensere  24734  blssioo  24760  tgioo  24761  xrtgioo  24772  xrsmopn  24778  zdis  24782  reperflem  24784  xrge0gsumle  24799  xrge0tsms  24800  icopnfhmeo  24910  bndth  24925  voliunlem2  25518  voliunlem3  25519  vitali  25580  ismbf3d  25621  itg2seq  25709  limccl  25842  limcresi  25852  dvef  25947  aasscn  26284  qssaa  26290  aannenlem2  26295  aannenlem3  26296  ulmcn  26364  mtestbdd  26370  iblulm  26372  reeff1o  26412  reefgim  26415  efifo  26511  dfrelog  26529  relogf1o  26530  logdmss  26606  logcn  26611  dvloglem  26612  logf1o2  26614  dvlog  26615  dvlog2lem  26616  dvlog2  26617  logtayl  26624  cxpcn  26709  cxpcn2  26710  cxpcn3  26712  resqrtcn  26713  efrlim  26933  dfef2  26934  cxp2lim  26940  basellem3  27046  basellem4  27047  sqff1o  27145  dchrmhm  27204  chtppilim  27438  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  dchrisumlema  27451  selberg2lem  27513  selberg3lem2  27521  pntrsumo1  27528  pnt2  27576  pnt  27577  madef  27828  oniso  28263  bdayn0sf1o  28362  dfnns2  28364  axcontlem2  29034  usgrexmplef  29328  griedg0ssusgr  29334  nbgrssvtx  29411  nbgrssovtx  29430  uvtxssvtx  29459  rgrusgrprc  29658  clwlkswks  29844  wwlkssswrd  29930  wwlkssswwlksn  29934  wspthsswwlkn  29986  wspthsswwlknon  29989  clwwlksclwwlkn  30101  phrel  30886  bnrel  30938  hlrel  30961  shex  31283  chsssh  31296  hhssnv  31335  choc1  31398  shunssi  31439  shsleji  31441  shsub1i  31443  shsub2i  31444  shsidmi  31455  omlsii  31474  spanuni  31615  spansni  31628  5oalem7  31731  3oalem3  31735  pjrni  31773  mayete3i  31799  hmopex  31946  cnlnssadj  32151  adjbdln  32154  adjsslnop  32158  shatomistici  32432  hatomistici  32433  xrge0tsmsd  33134  primefldchr  33362  1fldgenq  33383  zringidom  33611  esumpcvgval  34222  hashf2  34228  insiga  34281  sigapisys  34299  sigaldsys  34303  sigapildsys  34306  sxbrsigalem0  34415  dya2icobrsiga  34420  sxbrsigalem1  34429  sxbrsigalem2  34430  eulerpartlemb  34512  chtvalz  34773  logdivsqrle  34794  bnj1398  35176  bnj1498  35203  r1omfi  35248  fineqvacALT  35261  erdszelem9  35381  erdsze2lem2  35386  kur14lem9  35396  ptpconn  35415  iinllyconn  35436  cvmlift3  35510  mppsthm  35761  imagesset  36135  altxpsspw  36159  topjoin  36547  onsstopbas  36611  onsucconni  36619  onintopssconn  36622  onint1  36631  oninhaus  36632  ttcid  36674  dfttc4lem2  36711  dfttc4  36712  bj-snglss  37277  bj-imdirco  37504  bj-modssabl  37594  bj-rvecssmod  37610  bj-rvecssvec  37615  bj-rvecsscmod  37617  icoreunrn  37675  difunieq  37690  poimirlem8  37949  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem31  37972  poimirlem32  37973  heiborlem3  38134  disjsssrels  39257  atssbase  39736  readvrec2  42793  eldioph3b  43197  diophin  43204  diophun  43205  eldiophss  43206  isnumbasabl  43534  isnumbasgrp  43535  dfacbasgrp  43536  mon1psubm  43627  omssrncard  43967  inintabss  44005  intimass  44081  inaex  44724  nzin  44745  unipwrVD  45258  unipwr  45259  supxrre3  45755  fsumiunss  46005  rrpsscn  46018  dvnmul  46371  dvnprodlem2  46375  stoweidlem34  46462  stirlinglem13  46514  fourierdlem20  46555  fourierdlem62  46596  fourierdlem83  46617  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fouriersw  46659  qndenserrnbllem  46722  sge0iunmptlemre  46843  nn0ssge0  46852  sge0isum  46855  sge0seq  46874  sge0reuz  46875  caragendifcl  46942  carageniuncllem2  46950  hoicvrrex  46984  smfaddlem1  47191  smfaddlem2  47192  mbfpsssmf  47211  clnbgrssvtx  48307  srhmsubcALTV  48801  lvecpsslmod  48983  thincssc  49899  aacllem  50276  amgmwlem  50277  amgmlemALT  50278