Theorem ssriv 3919

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883

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

This theorem depends on definitions:  df-bi 208  df-ss 3900

This theorem is referenced by:  ssid  3937  ssv  3939  ssrab2  4011  difss  4066  ssun1  4107  inss1  4165  0ss  4328  difprsnss  4732  snsspw  4775  uniin  4862  pwuni  4876  iuniin  4934  iunpwss  5036  relopabi  5765  dmin  5853  dmrnssfld  5916  dmcoss  5917  dmcossOLD  5918  dminss  6104  imainss  6105  fvssunirn  6858  fviss  6904  opabresex2  7410  fvmptopab  7411  mapfoss  8789  fsetsspwxp  8790  mapsspm  8814  pmsspw  8815  uniixp  8859  pwfilem  9218  dffi3  9334  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  20532  subrgint  20567  srhmsubc  20652  subdrgint  20775  sdrgint  20776  primefld  20777  lssintcl  20954  prdslmodd  20959  cnsubmlem  21390  cnsubglem  21391  cnsubdrglem  21393  cnmsubglem  21405  xrge0subm  21418  zringunit  21441  zringlpir  21442  znf1o  21526  ocvss  21645  dsmmsubg  21718  dsmmlss  21719  lbslinds  21808  unitg  22950  cldss2  23013  indiscld  23074  iscldtop  23078  llyssnlly  23461  llyidm  23471  nllyidm  23472  toplly  23473  hauslly  23475  lly1stc  23479  dissnref  23511  txindis  23617  pthaus  23621  ptcmpfi  23796  ufinffr  23912  cnflf2  23986  flimfcls  24009  alexsubALTlem3  24032  ptcmplem1  24035  ptcmpg  24040  prdstmdd  24107  prdstgpd  24108  ust0  24203  prdsms  24514  qdensere  24752  blssioo  24778  tgioo  24779  xrtgioo  24790  xrsmopn  24796  zdis  24800  reperflem  24802  xrge0gsumle  24817  xrge0tsms  24818  icopnfhmeo  24928  bndth  24943  voliunlem2  25536  voliunlem3  25537  vitali  25598  ismbf3d  25639  itg2seq  25727  limccl  25860  limcresi  25870  dvef  25965  aasscn  26302  qssaa  26308  aannenlem2  26313  aannenlem3  26314  ulmcn  26382  mtestbdd  26388  iblulm  26390  reeff1o  26430  reefgim  26433  efifo  26529  dfrelog  26547  relogf1o  26548  logdmss  26624  logcn  26629  dvloglem  26630  logf1o2  26632  dvlog  26633  dvlog2lem  26634  dvlog2  26635  logtayl  26642  cxpcn  26727  cxpcn2  26728  cxpcn3  26730  resqrtcn  26731  efrlim  26951  dfef2  26952  cxp2lim  26958  basellem3  27064  basellem4  27065  sqff1o  27163  dchrmhm  27222  chtppilim  27456  chto1lb  27459  chpchtlim  27460  chpo1ub  27461  dchrisumlema  27469  selberg2lem  27531  selberg3lem2  27539  pntrsumo1  27546  pnt2  27594  pnt  27595  madef  27846  oniso  28281  bdayn0sf1o  28380  dfnns2  28382  axcontlem2  29052  usgrexmplef  29346  griedg0ssusgr  29352  nbgrssvtx  29429  nbgrssovtx  29448  uvtxssvtx  29477  rgrusgrprc  29676  clwlkswks  29862  wwlkssswrd  29948  wwlkssswwlksn  29952  wspthsswwlkn  30004  wspthsswwlknon  30007  clwwlksclwwlkn  30119  phrel  30904  bnrel  30956  hlrel  30979  shex  31301  chsssh  31314  hhssnv  31353  choc1  31416  shunssi  31457  shsleji  31459  shsub1i  31461  shsub2i  31462  shsidmi  31473  omlsii  31492  spanuni  31633  spansni  31646  5oalem7  31749  3oalem3  31753  pjrni  31791  mayete3i  31817  hmopex  31964  cnlnssadj  32169  adjbdln  32172  adjsslnop  32176  shatomistici  32450  hatomistici  32451  xrge0tsmsd  33154  primefldchr  33385  1fldgenq  33406  zringidom  33634  esumpcvgval  34262  hashf2  34268  insiga  34321  sigapisys  34339  sigaldsys  34343  sigapildsys  34346  sxbrsigalem0  34455  dya2icobrsiga  34460  sxbrsigalem1  34469  sxbrsigalem2  34470  eulerpartlemb  34552  chtvalz  34813  logdivsqrle  34834  bnj1398  35216  bnj1498  35243  r1omfi  35286  fineqvacALT  35298  erdszelem9  35427  erdsze2lem2  35432  kur14lem9  35442  ptpconn  35461  iinllyconn  35482  cvmlift3  35556  mppsthm  35807  imagesset  36181  altxpsspw  36205  topjoin  36593  onsstopbas  36657  onsucconni  36665  onintopssconn  36668  onint1  36677  oninhaus  36678  ttcid  36720  dfttc4lem2  36757  dfttc4  36758  bj-snglss  37323  bj-imdirco  37550  bj-modssabl  37640  bj-rvecssmod  37656  bj-rvecssvec  37661  bj-rvecsscmod  37663  icoreunrn  37721  difunieq  37736  poimirlem8  37995  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem31  38018  poimirlem32  38019  heiborlem3  38180  disjsssrels  39303  atssbase  39782  readvrec2  42838  eldioph3b  43214  diophin  43221  diophun  43222  eldiophss  43223  isnumbasabl  43551  isnumbasgrp  43552  dfacbasgrp  43553  mon1psubm  43644  omssrncard  43984  inintabss  44022  intimass  44098  inaex  44741  nzin  44762  unipwrVD  45275  unipwr  45276  supxrre3  45770  fsumiunss  46020  rrpsscn  46033  dvnmul  46386  dvnprodlem2  46390  stoweidlem34  46477  stirlinglem13  46529  fourierdlem20  46570  fourierdlem62  46611  fourierdlem83  46632  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fouriersw  46674  qndenserrnbllem  46737  sge0iunmptlemre  46858  nn0ssge0  46867  sge0isum  46870  sge0seq  46889  sge0reuz  46890  caragendifcl  46957  carageniuncllem2  46965  hoicvrrex  46999  smfaddlem1  47206  smfaddlem2  47207  mbfpsssmf  47226  clnbgrssvtx  48322  srhmsubcALTV  48816  lvecpsslmod  48998  thincssc  49914  aacllem  50291  amgmwlem  50292  amgmlemALT  50293