Theorem ssriv 3926

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

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

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 3907

This theorem is referenced by:  ssid  3944  ssv  3946  ssrab2  4018  difss  4073  ssun1  4114  inss1  4172  0ss  4335  difprsnss  4739  snsspw  4782  uniin  4869  pwuni  4883  iuniin  4941  iunpwss  5043  relopabi  5772  dmin  5860  dmrnssfld  5923  dmcoss  5924  dmcossOLD  5925  dminss  6111  imainss  6112  fvssunirn  6865  fviss  6911  opabresex2  7417  fvmptopab  7418  mapfoss  8796  fsetsspwxp  8797  mapsspm  8821  pmsspw  8822  uniixp  8866  pwfilem  9225  dffi3  9341  dfom3  9566  onwf  9752  tcrank  9806  djuss  9842  djuunxp  9843  djuun  9848  cardprclem  9901  alephsson  10020  ackbij1  10157  cardcf  10172  cfeq0  10176  dfacfin7  10319  hsmexlem6  10351  canthnum  10570  inaprc  10757  nqerf  10851  addnqf  10869  mulnqf  10870  dmrecnq  10889  reclem2pr  10969  wuncn  11091  zssre  12529  zsscn  12530  nnssz  12544  elq  12898  zssq  12904  qssre  12907  ixxssixx  13310  iooval2  13329  ioossre  13358  rge0ssre  13407  fzssz  13478  fz1ssnn  13507  fzssuz  13517  fzssp1  13519  uzdisj  13549  fz0ssnn0  13574  nn0disj  13596  fzossfz  13631  fzouzsplit  13647  fzo0ssnn0  13699  uzrdgfni  13918  seqcoll  14424  wrdexb  14485  fclim  15513  isercolllem3  15627  climcnds  15814  divcnv  15816  harmonic  15822  bitsss  16393  prmssnn  16643  prmssuz2  16664  maxprmfct  16677  1arith  16896  4sqlem19  16932  vdwlem12  16961  restsspw  17392  mremre  17564  mreacs  17622  isfunc  17829  homarel  18001  ledm  18554  lern  18555  chnexg  18582  smndex1basss  18874  sgrpssmgm  18902  mndsssgrp  18903  prdsgrpd  19024  prdsinvgd  19025  symgpssefmnd  19369  symgsubmefmndALT  19376  pgrpsubgsymg  19382  symgtrf  19442  odf1o2  19546  sylow3lem3  19602  sylow3lem6  19605  oppglsm  19615  efgsfo  19712  0frgp  19752  prdscmnd  19834  prdsabld  19835  dprdssv  19991  dprdres  20003  prdsrngd  20155  ringssrng  20265  prdsringd  20298  prdscrngd  20299  unitss  20354  subrngint  20539  subrgint  20574  srhmsubc  20659  subdrgint  20782  sdrgint  20783  primefld  20784  lssintcl  20961  prdslmodd  20966  cnsubmlem  21397  cnsubglem  21398  cnsubdrglem  21400  cnmsubglem  21412  xrge0subm  21425  zringunit  21448  zringlpir  21449  znf1o  21533  ocvss  21652  dsmmsubg  21725  dsmmlss  21726  lbslinds  21815  unitg  22957  cldss2  23020  indiscld  23081  iscldtop  23085  llyssnlly  23468  llyidm  23478  nllyidm  23479  toplly  23480  hauslly  23482  lly1stc  23486  dissnref  23518  txindis  23624  pthaus  23628  ptcmpfi  23803  ufinffr  23919  cnflf2  23993  flimfcls  24016  alexsubALTlem3  24039  ptcmplem1  24042  ptcmpg  24047  prdstmdd  24114  prdstgpd  24115  ust0  24210  prdsms  24521  qdensere  24759  blssioo  24785  tgioo  24786  xrtgioo  24797  xrsmopn  24803  zdis  24807  reperflem  24809  xrge0gsumle  24824  xrge0tsms  24825  icopnfhmeo  24935  bndth  24950  voliunlem2  25543  voliunlem3  25544  vitali  25605  ismbf3d  25646  itg2seq  25734  limccl  25867  limcresi  25877  dvef  25972  aasscn  26309  qssaa  26315  aannenlem2  26320  aannenlem3  26321  ulmcn  26389  mtestbdd  26395  iblulm  26397  reeff1o  26437  reefgim  26440  efifo  26536  dfrelog  26554  relogf1o  26555  logdmss  26631  logcn  26636  dvloglem  26637  logf1o2  26639  dvlog  26640  dvlog2lem  26641  dvlog2  26642  logtayl  26649  cxpcn  26734  cxpcn2  26735  cxpcn3  26737  resqrtcn  26738  efrlim  26958  dfef2  26959  cxp2lim  26965  basellem3  27071  basellem4  27072  sqff1o  27170  dchrmhm  27229  chtppilim  27463  chto1lb  27466  chpchtlim  27467  chpo1ub  27468  dchrisumlema  27476  selberg2lem  27538  selberg3lem2  27546  pntrsumo1  27553  pnt2  27601  pnt  27602  madef  27853  oniso  28288  bdayn0sf1o  28387  dfnns2  28389  axcontlem2  29059  usgrexmplef  29353  griedg0ssusgr  29359  nbgrssvtx  29436  nbgrssovtx  29455  uvtxssvtx  29484  rgrusgrprc  29683  clwlkswks  29869  wwlkssswrd  29955  wwlkssswwlksn  29959  wspthsswwlkn  30011  wspthsswwlknon  30014  clwwlksclwwlkn  30126  phrel  30911  bnrel  30963  hlrel  30986  shex  31308  chsssh  31321  hhssnv  31360  choc1  31423  shunssi  31464  shsleji  31466  shsub1i  31468  shsub2i  31469  shsidmi  31480  omlsii  31499  spanuni  31640  spansni  31653  5oalem7  31756  3oalem3  31760  pjrni  31798  mayete3i  31824  hmopex  31971  cnlnssadj  32176  adjbdln  32179  adjsslnop  32183  shatomistici  32457  hatomistici  32458  xrge0tsmsd  33161  primefldchr  33392  1fldgenq  33413  zringidom  33641  esumpcvgval  34269  hashf2  34275  insiga  34328  sigapisys  34346  sigaldsys  34350  sigapildsys  34353  sxbrsigalem0  34462  dya2icobrsiga  34467  sxbrsigalem1  34476  sxbrsigalem2  34477  eulerpartlemb  34559  chtvalz  34820  logdivsqrle  34841  bnj1398  35223  bnj1498  35250  r1omfi  35293  fineqvacALT  35305  erdszelem9  35434  erdsze2lem2  35439  kur14lem9  35449  ptpconn  35468  iinllyconn  35489  cvmlift3  35563  mppsthm  35814  imagesset  36188  altxpsspw  36212  topjoin  36600  onsstopbas  36664  onsucconni  36672  onintopssconn  36675  onint1  36684  oninhaus  36685  ttcid  36727  dfttc4lem2  36764  dfttc4  36765  bj-snglss  37330  bj-imdirco  37557  bj-modssabl  37647  bj-rvecssmod  37663  bj-rvecssvec  37668  bj-rvecsscmod  37670  icoreunrn  37728  difunieq  37743  poimirlem8  38002  poimirlem18  38012  poimirlem21  38015  poimirlem22  38016  poimirlem31  38025  poimirlem32  38026  heiborlem3  38187  disjsssrels  39310  atssbase  39789  readvrec2  42845  eldioph3b  43221  diophin  43228  diophun  43229  eldiophss  43230  isnumbasabl  43558  isnumbasgrp  43559  dfacbasgrp  43560  mon1psubm  43651  omssrncard  43991  inintabss  44029  intimass  44105  inaex  44748  nzin  44769  unipwrVD  45282  unipwr  45283  supxrre3  45777  fsumiunss  46027  rrpsscn  46040  dvnmul  46393  dvnprodlem2  46397  stoweidlem34  46484  stirlinglem13  46536  fourierdlem20  46577  fourierdlem62  46618  fourierdlem83  46639  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fouriersw  46681  qndenserrnbllem  46744  sge0iunmptlemre  46865  nn0ssge0  46874  sge0isum  46877  sge0seq  46896  sge0reuz  46897  caragendifcl  46964  carageniuncllem2  46972  hoicvrrex  47006  smfaddlem1  47213  smfaddlem2  47214  mbfpsssmf  47233  clnbgrssvtx  48329  srhmsubcALTV  48823  lvecpsslmod  49005  thincssc  49921  aacllem  50298  amgmwlem  50299  amgmlemALT  50300