Theorem ssriv 3943

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

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907

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

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

This theorem is referenced by:  ssid  3961  ssv  3963  ssrab2  4036  difss  4092  ssun1  4133  inss1  4191  0ss  4357  difprsnss  4762  snsspw  4805  uniinOLD  4893  pwuni  4907  iuniin  4965  iunpwss  5069  relopabi  5800  dmin  5892  dmrnssfld  5955  dmcoss  5956  dmcossOLD  5957  dminss  6142  imainss  6143  fvssunirn  6902  fviss  6948  opabresex2  7454  fvmptopab  7455  mapfoss  8837  fsetsspwxp  8838  mapsspm  8862  pmsspw  8863  uniixp  8907  pwfilem  9265  dffi3  9379  dfom3  9604  onwf  9790  tcrank  9844  djuss  9894  djuunxp  9895  djuun  9900  cardprclem  9953  alephsson  10072  ackbij1  10208  cardcf  10223  cfeq0  10228  dfacfin7  10371  hsmexlem6  10403  canthnum  10622  inaprc  10809  nqerf  10903  addnqf  10921  mulnqf  10922  dmrecnq  10941  reclem2pr  11021  wuncn  11143  zssre  12589  zsscn  12590  nnssz  12604  elq  12965  zssq  12971  qssre  12974  ixxssixx  13377  iooval2  13396  ioossre  13425  rge0ssre  13474  fzssz  13545  fz1ssnn  13574  fzssuz  13584  fzssp1  13586  uzdisj  13616  fz0ssnn0  13641  nn0disj  13663  fzossfz  13698  fzouzsplit  13714  fzo0ssnn0  13766  uzrdgfni  13985  seqcoll  14491  wrdexb  14552  fclim  15594  isercolllem3  15708  climcnds  15895  divcnv  15897  harmonic  15903  bitsss  16474  prmssnn  16724  prmssuz2  16745  maxprmfct  16758  1arith  16977  4sqlem19  17013  vdwlem12  17042  restsspw  17474  mremre  17646  mreacs  17704  isfunc  17911  homarel  18083  ledm  18636  lern  18637  chnexg  18664  smndex1basss  18957  sgrpssmgm  18985  mndsssgrp  18986  prdsgrpd  19107  prdsinvgd  19108  symgpssefmnd  19457  symgsubmefmndALT  19464  pgrpsubgsymg  19470  symgtrf  19530  odf1o2  19634  sylow3lem3  19690  sylow3lem6  19693  oppglsm  19703  efgsfo  19800  0frgp  19840  prdscmnd  19922  prdsabld  19923  dprdssv  20079  dprdres  20091  prdsrngd  20245  ringssrng  20360  prdsringd  20393  prdscrngd  20394  unitss  20449  subrngint  20636  subrgint  20671  srhmsubc  20756  subdrgint  20875  sdrgint  20876  primefld  20877  lssintcl  21054  prdslmodd  21059  cnsubmlem  21525  cnsubglem  21526  cnsubdrglem  21528  cnmsubglem  21540  xrge0subm  21553  zringunit  21576  zringlpir  21577  znf1o  21661  ocvss  21780  dsmmsubg  21853  dsmmlss  21854  lbslinds  21943  unitg  23085  cldss2  23148  indiscld  23209  iscldtop  23213  llyssnlly  23596  llyidm  23606  nllyidm  23607  toplly  23608  hauslly  23610  lly1stc  23614  dissnref  23646  txindis  23752  pthaus  23756  ptcmpfi  23931  ufinffr  24047  cnflf2  24121  flimfcls  24144  alexsubALTlem3  24167  ptcmplem1  24170  ptcmpg  24175  prdstmdd  24242  prdstgpd  24243  ust0  24338  prdsms  24649  qdensere  24887  blssioo  24913  tgioo  24914  xrtgioo  24925  xrsmopn  24931  zdis  24935  reperflem  24937  xrge0gsumle  24952  xrge0tsms  24953  icopnfhmeo  25063  bndth  25078  voliunlem2  25671  voliunlem3  25672  vitali  25733  ismbf3d  25774  itg2seq  25862  limccl  25995  limcresi  26005  dvef  26100  aasscn  26440  qssaa  26446  aannenlem2  26451  aannenlem3  26452  ulmcn  26520  mtestbdd  26526  iblulm  26528  reeff1o  26568  reefgim  26571  efifo  26670  dfrelog  26688  relogf1o  26689  logdmss  26765  logcn  26770  dvloglem  26771  logf1o2  26773  dvlog  26774  dvlog2lem  26775  dvlog2  26776  logtayl  26783  cxpcn  26868  cxpcn2  26869  cxpcn3  26871  resqrtcn  26872  efrlim  27092  dfef2  27093  cxp2lim  27099  basellem3  27205  basellem4  27206  sqff1o  27304  dchrmhm  27363  chtppilim  27597  chto1lb  27600  chpchtlim  27601  chpo1ub  27602  dchrisumlema  27610  selberg2lem  27672  selberg3lem2  27680  pntrsumo1  27687  pnt2  27735  pnt  27736  madef  27987  oniso  28422  bdayn0sf1o  28521  dfnns2  28523  axcontlem2  29224  usgrexmplef  29518  griedg0ssusgr  29524  nbgrssvtx  29601  nbgrssovtx  29620  uvtxssvtx  29649  rgrusgrprc  29848  clwlkswks  30034  wwlkssswrd  30120  wwlkssswwlksn  30124  wspthsswwlkn  30176  wspthsswwlknon  30179  clwwlksclwwlkn  30291  phrel  31076  bnrel  31128  hlrel  31151  shex  31473  chsssh  31486  hhssnv  31525  choc1  31588  shunssi  31629  shsleji  31631  shsub1i  31633  shsub2i  31634  shsidmi  31645  omlsii  31664  spanuni  31805  spansni  31818  5oalem7  31921  3oalem3  31925  pjrni  31963  mayete3i  31989  hmopex  32136  cnlnssadj  32341  adjbdln  32344  adjsslnop  32348  shatomistici  32622  hatomistici  32623  xrge0tsmsd  33306  primefldchr  33537  1fldgenq  33558  zringidom  33758  esumpcvgval  34385  hashf2  34391  insiga  34444  sigapisys  34462  sigaldsys  34466  sigapildsys  34469  sxbrsigalem0  34578  dya2icobrsiga  34583  sxbrsigalem1  34592  sxbrsigalem2  34593  eulerpartlemb  34675  chtvalz  34933  logdivsqrle  34954  bnj1398  35339  bnj1498  35366  r1omfi  35413  fineqvacALT  35425  erdszelem9  35562  erdsze2lem2  35567  kur14lem9  35577  ptpconn  35596  iinllyconn  35617  cvmlift3  35691  mppsthm  35942  imagesset  36316  altxpsspw  36340  topjoin  36738  onsstopbas  36802  onsucconni  36810  onintopssconn  36813  onint1  36822  oninhaus  36823  ttcid  36865  dfttc4lem2  36902  dfttc4  36903  bj-snglss  37467  bj-imdirco  37694  bj-modssabl  37784  bj-rvecssmod  37800  bj-rvecssvec  37805  bj-rvecsscmod  37807  icoreunrn  37865  difunieq  37880  poimirlem8  38139  poimirlem18  38149  poimirlem21  38152  poimirlem22  38153  poimirlem31  38162  poimirlem32  38163  heiborlem3  38324  disjsssrels  39447  atssbase  39926  readvrec2  42982  eldioph3b  43358  diophin  43365  diophun  43366  eldiophss  43367  isnumbasabl  43695  isnumbasgrp  43696  dfacbasgrp  43697  mon1psubm  43788  omssrncard  44128  inintabss  44166  intimass  44242  inaex  44871  nzin  44892  unipwrVD  45405  unipwr  45406  supxrre3  45899  fsumiunss  46149  rrpsscn  46162  dvnmul  46515  dvnprodlem2  46519  stoweidlem34  46606  stirlinglem13  46658  fourierdlem20  46699  fourierdlem62  46740  fourierdlem83  46761  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fouriersw  46803  qndenserrnbllem  46866  sge0iunmptlemre  46987  nn0ssge0  46996  sge0isum  46999  sge0seq  47018  sge0reuz  47019  caragendifcl  47086  carageniuncllem2  47094  hoicvrrex  47128  smfaddlem1  47335  smfaddlem2  47336  mbfpsssmf  47355  clnbgrssvtx  48451  srhmsubcALTV  48945  lvecpsslmod  49138  thincssc  50053  aacllem  50430  amgmwlem  50431  amgmlemALT  50432