Theorem ssriv 3935

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ss 3916

This theorem is used by:  ssid  3953  ssv  3955  ssrab2  4028  difss  4083  ssun1  4124  inss1  4182  0ss  4350  difprsnss  4762  snsspw  4804  uniinOLD  4892  pwuni  4906  iuniin  4964  iunpwss  5067  relopabi  5800  dmin  5893  dmrnssfld  5956  dmcoss  5957  dmcossOLD  5958  dminss  6142  imainss  6143  fvssunirn  6908  fviss  6954  opabresex2  7466  fvmptopab  7467  mapfoss  8858  fsetsspwxp  8859  mapsspm  8888  pmsspw  8889  uniixp  8933  pwfilem  9293  dffi3  9407  dfom3  9632  onwf  9821  tcrank  9882  hfuni  9905  djuss  9982  djuunxp  9983  djuun  9988  cardprclem  10041  alephsson  10160  ackbij1  10296  cardcf  10310  cfeq0  10315  dfacfin7  10458  hsmexlem6  10490  canthnum  10715  inaprc  10902  nqerf  10996  addnqf  11014  mulnqf  11015  dmrecnq  11034  reclem2pr  11114  wuncn  11236  zssre  12681  zsscn  12682  nnssz  12696  elq  13058  zssq  13064  qssre  13067  ixxssixx  13471  iooval2  13490  ioossre  13519  rge0ssre  13568  fzssz  13639  fz1ssnn  13669  fzssuz  13679  fzssp1  13681  uzdisj  13711  fz0ssnn0  13736  nn0disj  13758  fzossfz  13793  fzouzsplit  13809  fzo0ssnn0  13861  uzrdgfni  14081  seqcoll  14589  wrdexb  14650  fclim  15700  isercolllem3  15814  climcnds  16000  divcnv  16002  harmonic  16008  bitsss  16576  prmssnn  16831  prmssuz2  16852  maxprmfct  16865  1arith  17085  4sqlem19  17121  vdwlem12  17150  restsspw  17582  mremre  17754  mreacs  17812  isfunc  18019  homarel  18191  ledm  18744  lern  18745  chnexg  18772  smndex1basss  19084  sgrpssmgm  19112  mndsssgrp  19113  prdsgrpd  19240  prdsinvgd  19241  symgpssefmnd  19590  symgsubmefmndALT  19597  pgrpsubgsymg  19603  symgtrf  19663  odf1o2  19767  sylow3lem3  19823  sylow3lem6  19826  oppglsm  19836  efgsfo  19933  0frgp  19973  prdscmnd  20055  prdsabld  20056  dprdssv  20212  dprdres  20224  prdsrngd  20378  ringssrng  20495  prdsringd  20530  prdscrngd  20531  unitss  20586  subrngint  20792  subrgint  20827  srhmsubc  20912  subdrgint  21040  sdrgint  21041  primefld  21042  lssintcl  21219  prdslmodd  21224  cnsubmlem  21701  cnsubglem  21702  cnsubdrglem  21704  cnmsubglem  21716  xrge0subm  21729  zringunit  21752  zringlpir  21753  znf1o  21837  ocvss  21956  dsmmsubg  22029  dsmmlss  22030  lbslinds  22119  unitg  23265  cldss2  23328  indiscld  23389  iscldtop  23393  llyssnlly  23777  llyidm  23787  nllyidm  23788  toplly  23789  hauslly  23791  lly1stc  23795  dissnref  23827  txindis  23933  pthaus  23937  ptcmpfi  24112  ufinffr  24228  cnflf2  24302  flimfcls  24325  alexsubALTlem3  24348  ptcmplem1  24351  ptcmpg  24356  prdstmdd  24423  prdstgpd  24424  ust0  24519  prdsms  24830  qdensere  25068  blssioo  25094  tgioo  25095  xrtgioo  25106  xrsmopn  25112  zdis  25116  reperflem  25118  xrge0gsumle  25133  xrge0tsms  25134  icopnfhmeo  25244  bndth  25259  voliunlem2  25852  voliunlem3  25853  vitali  25914  ismbf3d  25955  itg2seq  26043  limccl  26175  limcresi  26185  dvef  26280  aasscn  26623  qssaa  26630  aannenlem2  26638  aannenlem3  26639  ulmcn  26708  mtestbdd  26714  iblulm  26716  reeff1o  26756  reefgim  26759  efifo  26857  dfrelog  26875  relogf1o  26876  logdmss  26952  logcn  26957  dvloglem  26958  logf1o2  26960  dvlog  26961  dvlog2lem  26962  dvlog2  26963  logtayl  26970  cxpcn  27055  cxpcn2  27056  cxpcn3  27058  resqrtcn  27059  efrlim  27279  dfef2  27280  cxp2lim  27286  basellem3  27392  basellem4  27393  sqff1o  27491  dchrmhm  27550  chtppilim  27784  chto1lb  27787  chpchtlim  27788  chpo1ub  27789  dchrisumlema  27797  selberg2lem  27859  selberg3lem2  27867  pntrsumo1  27874  pnt2  27922  pnt  27923  madef  28204  oniso  28639  bdayn0sf1o  28738  dfnns2  28740  axcontlem2  29525  usgrexmplef  29822  griedg0ssusgr  29828  nbgrssvtx  29905  nbgrssovtx  29924  uvtxssvtx  29953  rgrusgrprc  30152  clwlkswks  30345  wwlkssswrd  30433  wwlkssswwlksn  30437  wspthsswwlkn  30489  wspthsswwlknon  30492  clwwlksclwwlkn  30604  phrel  31399  bnrel  31451  hlrel  31474  shex  31796  chsssh  31809  hhssnv  31848  choc1  31911  shunssi  31952  shsleji  31954  shsub1i  31956  shsub2i  31957  shsidmi  31968  omlsii  31987  spanuni  32128  spansni  32141  5oalem7  32244  3oalem3  32248  pjrni  32286  mayete3i  32312  hmopex  32459  cnlnssadj  32664  adjbdln  32667  adjsslnop  32671  shatomistici  32945  hatomistici  32946  xrge0tsmsd  33616  primefldchr  33845  1fldgenq  33866  zringidom  34065  esumpcvgval  34692  hashf2  34698  insiga  34752  sigapisys  34770  sigaldsys  34774  sigapildsys  34777  sxbrsigalem0  34886  dya2icobrsiga  34891  sxbrsigalem1  34900  sxbrsigalem2  34901  eulerpartlemb  34983  chtvalz  35241  logdivsqrle  35262  bnj1398  35647  bnj1498  35674  r1omfi  35709  fineqvacALT  35758  erdszelem9  35933  erdsze2lem2  35938  kur14lem9  35948  ptpconn  35967  iinllyconn  35988  cvmlift3  36062  mppsthm  36313  imagesset  36687  altxpsspw  36712  topjoin  37123  onsstopbas  37187  onsucconni  37195  onintopssconn  37198  onint1  37207  oninhaus  37208  ttcid  37250  dfttc4lem2  37287  dfttc4  37288  bj-snglss  37853  bj-imdirco  38079  bj-modssabl  38169  bj-rvecssmod  38185  bj-rvecssvec  38190  bj-rvecsscmod  38192  icoreunrn  38250  difunieq  38265  poimirlem8  38514  poimirlem18  38524  poimirlem21  38527  poimirlem22  38528  poimirlem31  38537  poimirlem32  38538  heiborlem3  38715  disjsssrels  39836  atssbase  40315  readvrec2  43380  eldioph3b  43729  diophin  43736  diophun  43737  eldiophss  43738  isnumbasabl  44066  isnumbasgrp  44067  dfacbasgrp  44068  mon1psubm  44159  omssrncard  44499  inintabss  44537  intimass  44613  inaex  45240  nzin  45261  unipwrVD  45773  unipwr  45774  omsshf  45974  supxrre3  46281  fsumiunss  46531  rrpsscn  46544  dvnmul  46897  dvnprodlem2  46901  stoweidlem34  46988  stirlinglem13  47040  fourierdlem20  47081  fourierdlem62  47122  fourierdlem83  47143  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fouriersw  47185  qndenserrnbllem  47248  sge0iunmptlemre  47369  nn0ssge0  47378  sge0isum  47381  sge0seq  47400  sge0reuz  47401  caragendifcl  47468  carageniuncllem2  47476  hoicvrrex  47510  smfaddlem1  47717  smfaddlem2  47718  mbfpsssmf  47737  wrddun2  47844  chndun2  47849  chnrun2  47854  clnbgrssvtx  48873  srhmsubcALTV  49366  lvecpsslmod  49563  thincssc  50476  aacllem  50883  amgmwlem  50931  amgmlemALT  50932