Theorem ssriv 3942

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-ss 3923

This theorem is referenced by:  ssid  3960  ssv  3962  ssrab2  4035  difss  4091  ssun1  4132  inss1  4190  0ss  4358  difprsnss  4768  snsspw  4810  uniinOLD  4898  pwuni  4912  iuniin  4970  iunpwss  5074  relopabi  5811  dmin  5903  dmrnssfld  5966  dmcoss  5967  dmcossOLD  5968  dminss  6152  imainss  6153  fvssunirn  6914  fviss  6960  opabresex2  7466  fvmptopab  7467  mapfoss  8850  fsetsspwxp  8851  mapsspm  8875  pmsspw  8876  uniixp  8920  pwfilem  9278  dffi3  9392  dfom3  9617  onwf  9803  tcrank  9857  djuss  9907  djuunxp  9908  djuun  9913  cardprclem  9966  alephsson  10085  ackbij1  10221  cardcf  10236  cfeq0  10241  dfacfin7  10384  hsmexlem6  10416  canthnum  10635  inaprc  10822  nqerf  10916  addnqf  10934  mulnqf  10935  dmrecnq  10954  reclem2pr  11034  wuncn  11156  zssre  12599  zsscn  12600  nnssz  12614  elq  12975  zssq  12981  qssre  12984  ixxssixx  13387  iooval2  13406  ioossre  13435  rge0ssre  13484  fzssz  13555  fz1ssnn  13585  fzssuz  13595  fzssp1  13597  uzdisj  13627  fz0ssnn0  13652  nn0disj  13674  fzossfz  13709  fzouzsplit  13725  fzo0ssnn0  13777  uzrdgfni  13996  seqcoll  14503  wrdexb  14564  fclim  15606  isercolllem3  15720  climcnds  15907  divcnv  15909  harmonic  15915  bitsss  16485  prmssnn  16735  prmssuz2  16756  maxprmfct  16769  1arith  16988  4sqlem19  17024  vdwlem12  17053  restsspw  17485  mremre  17657  mreacs  17715  isfunc  17922  homarel  18094  ledm  18647  lern  18648  chnexg  18675  smndex1basss  18968  sgrpssmgm  18996  mndsssgrp  18997  prdsgrpd  19117  prdsinvgd  19118  symgpssefmnd  19467  symgsubmefmndALT  19474  pgrpsubgsymg  19480  symgtrf  19540  odf1o2  19644  sylow3lem3  19700  sylow3lem6  19703  oppglsm  19713  efgsfo  19810  0frgp  19850  prdscmnd  19932  prdsabld  19933  dprdssv  20089  dprdres  20101  prdsrngd  20255  ringssrng  20370  prdsringd  20403  prdscrngd  20404  unitss  20459  subrngint  20646  subrgint  20681  srhmsubc  20766  subdrgint  20887  sdrgint  20888  primefld  20889  lssintcl  21066  prdslmodd  21071  cnsubmlem  21546  cnsubglem  21547  cnsubdrglem  21549  cnmsubglem  21561  xrge0subm  21574  zringunit  21597  zringlpir  21598  znf1o  21682  ocvss  21801  dsmmsubg  21874  dsmmlss  21875  lbslinds  21964  unitg  23105  cldss2  23168  indiscld  23229  iscldtop  23233  llyssnlly  23616  llyidm  23626  nllyidm  23627  toplly  23628  hauslly  23630  lly1stc  23634  dissnref  23666  txindis  23772  pthaus  23776  ptcmpfi  23951  ufinffr  24067  cnflf2  24141  flimfcls  24164  alexsubALTlem3  24187  ptcmplem1  24190  ptcmpg  24195  prdstmdd  24262  prdstgpd  24263  ust0  24358  prdsms  24669  qdensere  24907  blssioo  24933  tgioo  24934  xrtgioo  24945  xrsmopn  24951  zdis  24955  reperflem  24957  xrge0gsumle  24972  xrge0tsms  24973  icopnfhmeo  25083  bndth  25098  voliunlem2  25691  voliunlem3  25692  vitali  25753  ismbf3d  25794  itg2seq  25882  limccl  26015  limcresi  26025  dvef  26120  aasscn  26460  qssaa  26466  aannenlem2  26471  aannenlem3  26472  ulmcn  26540  mtestbdd  26546  iblulm  26548  reeff1o  26588  reefgim  26591  efifo  26690  dfrelog  26708  relogf1o  26709  logdmss  26785  logcn  26790  dvloglem  26791  logf1o2  26793  dvlog  26794  dvlog2lem  26795  dvlog2  26796  logtayl  26803  cxpcn  26888  cxpcn2  26889  cxpcn3  26891  resqrtcn  26892  efrlim  27112  dfef2  27113  cxp2lim  27119  basellem3  27225  basellem4  27226  sqff1o  27324  dchrmhm  27383  chtppilim  27617  chto1lb  27620  chpchtlim  27621  chpo1ub  27622  dchrisumlema  27630  selberg2lem  27692  selberg3lem2  27700  pntrsumo1  27707  pnt2  27755  pnt  27756  madef  28007  oniso  28442  bdayn0sf1o  28541  dfnns2  28543  axcontlem2  29293  usgrexmplef  29587  griedg0ssusgr  29593  nbgrssvtx  29670  nbgrssovtx  29689  uvtxssvtx  29718  rgrusgrprc  29917  clwlkswks  30103  wwlkssswrd  30189  wwlkssswwlksn  30193  wspthsswwlkn  30245  wspthsswwlknon  30248  clwwlksclwwlkn  30360  phrel  31145  bnrel  31197  hlrel  31220  shex  31542  chsssh  31555  hhssnv  31594  choc1  31657  shunssi  31698  shsleji  31700  shsub1i  31702  shsub2i  31703  shsidmi  31714  omlsii  31733  spanuni  31874  spansni  31887  5oalem7  31990  3oalem3  31994  pjrni  32032  mayete3i  32058  hmopex  32205  cnlnssadj  32410  adjbdln  32413  adjsslnop  32417  shatomistici  32691  hatomistici  32692  xrge0tsmsd  33371  primefldchr  33600  1fldgenq  33621  zringidom  33819  esumpcvgval  34446  hashf2  34452  insiga  34505  sigapisys  34523  sigaldsys  34527  sigapildsys  34530  sxbrsigalem0  34639  dya2icobrsiga  34644  sxbrsigalem1  34653  sxbrsigalem2  34654  eulerpartlemb  34736  chtvalz  34994  logdivsqrle  35015  bnj1398  35400  bnj1498  35427  r1omfi  35477  fineqvacALT  35508  erdszelem9  35669  erdsze2lem2  35674  kur14lem9  35684  ptpconn  35703  iinllyconn  35724  cvmlift3  35798  mppsthm  36049  imagesset  36423  altxpsspw  36447  topjoin  36854  onsstopbas  36918  onsucconni  36926  onintopssconn  36929  onint1  36938  oninhaus  36939  ttcid  36981  dfttc4lem2  37018  dfttc4  37019  bj-snglss  37584  bj-imdirco  37812  bj-modssabl  37902  bj-rvecssmod  37918  bj-rvecssvec  37923  bj-rvecsscmod  37925  icoreunrn  37983  difunieq  37998  poimirlem8  38257  poimirlem18  38267  poimirlem21  38270  poimirlem22  38271  poimirlem31  38280  poimirlem32  38281  heiborlem3  38442  disjsssrels  39563  atssbase  40042  readvrec2  43100  eldioph3b  43476  diophin  43483  diophun  43484  eldiophss  43485  isnumbasabl  43813  isnumbasgrp  43814  dfacbasgrp  43815  mon1psubm  43906  omssrncard  44246  inintabss  44284  intimass  44360  inaex  44987  nzin  45008  unipwrVD  45520  unipwr  45521  supxrre3  46021  fsumiunss  46271  rrpsscn  46284  dvnmul  46637  dvnprodlem2  46641  stoweidlem34  46728  stirlinglem13  46780  fourierdlem20  46821  fourierdlem62  46862  fourierdlem83  46883  fourierdlem101  46901  fourierdlem103  46903  fourierdlem104  46904  fourierdlem111  46911  fouriersw  46925  qndenserrnbllem  46988  sge0iunmptlemre  47109  nn0ssge0  47118  sge0isum  47121  sge0seq  47140  sge0reuz  47141  caragendifcl  47208  carageniuncllem2  47216  hoicvrrex  47250  smfaddlem1  47457  smfaddlem2  47458  mbfpsssmf  47477  clnbgrssvtx  48573  srhmsubcALTV  49067  lvecpsslmod  49264  thincssc  50179  aacllem  50578  amgmwlem  50579  amgmlemALT  50580