Theorem ssriv 3939

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903

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

This theorem depends on definitions:  df-bi 207  df-ss 3920

This theorem is referenced by:  ssid  3958  ssv  3960  ssrab2  4034  difss  4090  ssun1  4132  inss1  4191  0ss  4354  difprsnss  4757  snsspw  4802  uniin  4889  pwuni  4903  iuniin  4961  iunpwss  5064  relopabi  5779  dmin  5868  dmrnssfld  5931  dmcoss  5932  dmcossOLD  5933  dminss  6119  imainss  6120  fvssunirn  6873  fviss  6919  opabresex2  7422  fvmptopab  7423  mapfoss  8801  fsetsspwxp  8802  mapsspm  8826  pmsspw  8827  uniixp  8871  pwfilem  9230  dffi3  9346  dfom3  9568  onwf  9754  tcrank  9808  djuss  9844  djuunxp  9845  djuun  9850  cardprclem  9903  alephsson  10022  ackbij1  10159  cardcf  10174  cfeq0  10178  dfacfin7  10321  hsmexlem6  10353  canthnum  10572  inaprc  10759  nqerf  10853  addnqf  10871  mulnqf  10872  dmrecnq  10891  reclem2pr  10971  wuncn  11093  zssre  12507  zsscn  12508  nnssz  12522  elq  12875  zssq  12881  qssre  12884  ixxssixx  13287  iooval2  13306  ioossre  13335  rge0ssre  13384  fzssz  13454  fz1ssnn  13483  fzssuz  13493  fzssp1  13495  uzdisj  13525  fz0ssnn0  13550  nn0disj  13572  fzossfz  13606  fzouzsplit  13622  fzo0ssnn0  13674  uzrdgfni  13893  seqcoll  14399  wrdexb  14460  fclim  15488  isercolllem3  15602  climcnds  15786  divcnv  15788  harmonic  15794  bitsss  16365  prmssnn  16615  maxprmfct  16648  1arith  16867  4sqlem19  16903  vdwlem12  16932  restsspw  17363  mremre  17535  mreacs  17593  isfunc  17800  homarel  17972  ledm  18525  lern  18526  chnexg  18553  smndex1basss  18842  sgrpssmgm  18870  mndsssgrp  18871  prdsgrpd  18992  prdsinvgd  18993  symgpssefmnd  19337  symgsubmefmndALT  19344  pgrpsubgsymg  19350  symgtrf  19410  odf1o2  19514  sylow3lem3  19570  sylow3lem6  19573  oppglsm  19583  efgsfo  19680  0frgp  19720  prdscmnd  19802  prdsabld  19803  dprdssv  19959  dprdres  19971  prdsrngd  20123  ringssrng  20233  prdsringd  20268  prdscrngd  20269  unitss  20324  subrngint  20505  subrgint  20540  srhmsubc  20625  subdrgint  20748  sdrgint  20749  primefld  20750  lssintcl  20927  prdslmodd  20932  cnsubmlem  21381  cnsubglem  21382  cnsubdrglem  21385  cnmsubglem  21397  xrge0subm  21410  zringunit  21433  zringlpir  21434  znf1o  21518  ocvss  21637  dsmmsubg  21710  dsmmlss  21711  lbslinds  21800  unitg  22923  cldss2  22986  indiscld  23047  iscldtop  23051  llyssnlly  23434  llyidm  23444  nllyidm  23445  toplly  23446  hauslly  23448  lly1stc  23452  dissnref  23484  txindis  23590  pthaus  23594  ptcmpfi  23769  ufinffr  23885  cnflf2  23959  flimfcls  23982  alexsubALTlem3  24005  ptcmplem1  24008  ptcmpg  24013  prdstmdd  24080  prdstgpd  24081  ust0  24176  prdsms  24487  qdensere  24725  blssioo  24751  tgioo  24752  xrtgioo  24763  xrsmopn  24769  zdis  24773  reperflem  24775  xrge0gsumle  24790  xrge0tsms  24791  icopnfhmeo  24909  bndth  24925  voliunlem2  25520  voliunlem3  25521  vitali  25582  ismbf3d  25623  itg2seq  25711  limccl  25844  limcresi  25854  dvef  25952  aasscn  26294  qssaa  26300  aannenlem2  26305  aannenlem3  26306  ulmcn  26376  mtestbdd  26382  iblulm  26384  reeff1o  26425  reefgim  26428  efifo  26524  dfrelog  26542  relogf1o  26543  logdmss  26619  logcn  26624  dvloglem  26625  logf1o2  26627  dvlog  26628  dvlog2lem  26629  dvlog2  26630  logtayl  26637  cxpcn  26722  cxpcnOLD  26723  cxpcn2  26724  cxpcn3  26726  resqrtcn  26727  efrlim  26947  efrlimOLD  26948  dfef2  26949  cxp2lim  26955  basellem3  27061  basellem4  27062  sqff1o  27160  dchrmhm  27220  chtppilim  27454  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  dchrisumlema  27467  selberg2lem  27529  selberg3lem2  27537  pntrsumo1  27544  pnt2  27592  pnt  27593  madef  27844  oniso  28279  bdayn0sf1o  28378  dfnns2  28380  axcontlem2  29050  usgrexmplef  29344  griedg0ssusgr  29350  nbgrssvtx  29427  nbgrssovtx  29446  uvtxssvtx  29475  rgrusgrprc  29675  clwlkswks  29861  wwlkssswrd  29947  wwlkssswwlksn  29951  wspthsswwlkn  30003  wspthsswwlknon  30006  clwwlksclwwlkn  30118  phrel  30902  bnrel  30954  hlrel  30977  shex  31299  chsssh  31312  hhssnv  31351  choc1  31414  shunssi  31455  shsleji  31457  shsub1i  31459  shsub2i  31460  shsidmi  31471  omlsii  31490  spanuni  31631  spansni  31644  5oalem7  31747  3oalem3  31751  pjrni  31789  mayete3i  31815  hmopex  31962  cnlnssadj  32167  adjbdln  32170  adjsslnop  32174  shatomistici  32448  hatomistici  32449  xrge0tsmsd  33166  primefldchr  33394  1fldgenq  33415  zringidom  33643  esumpcvgval  34255  hashf2  34261  insiga  34314  sigapisys  34332  sigaldsys  34336  sigapildsys  34339  sxbrsigalem0  34448  dya2icobrsiga  34453  sxbrsigalem1  34462  sxbrsigalem2  34463  eulerpartlemb  34545  chtvalz  34806  logdivsqrle  34827  bnj1398  35209  bnj1498  35236  r1omfi  35280  fineqvacALT  35292  erdszelem9  35412  erdsze2lem2  35417  kur14lem9  35427  ptpconn  35446  iinllyconn  35467  cvmlift3  35541  mppsthm  35792  imagesset  36166  altxpsspw  36190  topjoin  36578  onsstopbas  36642  onsucconni  36650  onintopssconn  36653  onint1  36662  oninhaus  36663  bj-snglss  37212  bj-imdirco  37439  bj-modssabl  37529  bj-rvecssmod  37545  bj-rvecssvec  37550  bj-rvecsscmod  37552  icoreunrn  37608  difunieq  37623  poimirlem8  37873  poimirlem18  37883  poimirlem21  37886  poimirlem22  37887  poimirlem31  37896  poimirlem32  37897  heiborlem3  38058  disjsssrels  39181  atssbase  39660  readvrec2  42725  eldioph3b  43116  diophin  43123  diophun  43124  eldiophss  43125  isnumbasabl  43457  isnumbasgrp  43458  dfacbasgrp  43459  mon1psubm  43550  omssrncard  43890  inintabss  43928  intimass  44004  inaex  44647  nzin  44668  unipwrVD  45181  unipwr  45182  supxrre3  45678  fsumiunss  45929  rrpsscn  45942  dvnmul  46295  dvnprodlem2  46299  stoweidlem34  46386  stirlinglem13  46438  fourierdlem20  46479  fourierdlem62  46520  fourierdlem83  46541  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fouriersw  46583  qndenserrnbllem  46646  sge0iunmptlemre  46767  nn0ssge0  46776  sge0isum  46779  sge0seq  46798  sge0reuz  46799  caragendifcl  46866  carageniuncllem2  46874  hoicvrrex  46908  smfaddlem1  47115  smfaddlem2  47116  mbfpsssmf  47135  clnbgrssvtx  48185  srhmsubcALTV  48679  lvecpsslmod  48861  thincssc  49777  aacllem  50154  amgmwlem  50155  amgmlemALT  50156