Theorem ssriv 3905

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  ssid  3923  ssv  3925  ssrab2  3993  difss  4046  ssun1  4086  inss1  4143  0ss  4311  difprsnss  4712  snsspw  4755  uniin  4845  pwuni  4858  iuniin  4916  iunpwss  5015  pwunssOLD  5450  relopabi  5692  dmin  5780  dmrnssfld  5839  dmcoss  5840  dminss  6016  imainss  6017  fviss  6788  mapfoss  8533  fsetsspwxp  8534  mapsspm  8557  pmsspw  8558  uniixp  8602  pwfilem  8855  pwfilemOLD  8970  dffi3  9047  dfom3  9262  onwf  9446  tcrank  9500  djuss  9536  djuunxp  9537  djuun  9542  cardprclem  9595  alephsson  9714  ackbij1  9852  cardcf  9866  cfeq0  9870  dfacfin7  10013  hsmexlem6  10045  canthnum  10263  inaprc  10450  nqerf  10544  addnqf  10562  mulnqf  10563  dmrecnq  10582  reclem2pr  10662  wuncn  10784  zssre  12183  zsscn  12184  nnssz  12197  elq  12546  zssq  12552  qssre  12555  ixxssixx  12949  iooval2  12968  ioossre  12996  rge0ssre  13044  fzssz  13114  fz1ssnn  13143  fzssuz  13153  fzssp1  13155  uzdisj  13185  fz0ssnn0  13207  nn0disj  13228  fzossfz  13261  fzouzsplit  13277  fzo0ssnn0  13323  uzrdgfni  13531  seqcoll  14030  wrdexb  14080  fclim  15114  isercolllem3  15230  climcnds  15415  divcnv  15417  harmonic  15423  bitsss  15985  prmssnn  16233  maxprmfct  16266  1arith  16480  4sqlem19  16516  vdwlem12  16545  restsspw  16936  mremre  17107  mreacs  17161  isfunc  17370  homarel  17542  ledm  18096  lern  18097  smndex1basss  18332  sgrpssmgm  18360  mndsssgrp  18361  prdsgrpd  18473  prdsinvgd  18474  symgpssefmnd  18788  symgsubmefmndALT  18795  pgrpsubgsymg  18801  symgtrf  18861  odf1o2  18962  sylow3lem3  19018  sylow3lem6  19021  oppglsm  19031  efgsfo  19129  0frgp  19169  prdscmnd  19246  prdsabld  19247  dprdssv  19403  dprdres  19415  prdsringd  19630  prdscrngd  19631  unitss  19678  subrgint  19822  subdrgint  19847  sdrgint  19848  primefld  19849  lssintcl  20001  prdslmodd  20006  xrge0subm  20404  cnsubmlem  20411  cnsubglem  20412  cnsubdrglem  20414  cnmsubglem  20426  zringunit  20453  zringlpir  20454  znf1o  20516  ocvss  20632  dsmmsubg  20705  dsmmlss  20706  lbslinds  20795  unitg  21864  cldss2  21927  indiscld  21988  iscldtop  21992  llyssnlly  22375  llyidm  22385  nllyidm  22386  toplly  22387  hauslly  22389  lly1stc  22393  dissnref  22425  txindis  22531  pthaus  22535  ptcmpfi  22710  ufinffr  22826  cnflf2  22900  flimfcls  22923  alexsubALTlem3  22946  ptcmplem1  22949  ptcmpg  22954  prdstmdd  23021  prdstgpd  23022  ust0  23117  prdsms  23429  qdensere  23667  blssioo  23692  tgioo  23693  xrtgioo  23703  xrsmopn  23709  zdis  23713  reperflem  23715  xrge0gsumle  23730  xrge0tsms  23731  icopnfhmeo  23840  bndth  23855  voliunlem2  24448  voliunlem3  24449  vitali  24510  ismbf3d  24551  itg2seq  24640  limccl  24772  limcresi  24782  dvef  24877  aasscn  25211  qssaa  25217  aannenlem2  25222  aannenlem3  25223  ulmcn  25291  mtestbdd  25297  iblulm  25299  reeff1o  25339  reefgim  25342  efifo  25436  dfrelog  25454  relogf1o  25455  logdmss  25530  logcn  25535  dvloglem  25536  logf1o2  25538  dvlog  25539  dvlog2lem  25540  dvlog2  25541  logtayl  25548  cxpcn  25631  cxpcn2  25632  cxpcn3  25634  resqrtcn  25635  efrlim  25852  dfef2  25853  cxp2lim  25859  basellem3  25965  basellem4  25966  sqff1o  26064  dchrmhm  26122  chtppilim  26356  chto1lb  26359  chpchtlim  26360  chpo1ub  26361  dchrisumlema  26369  selberg2lem  26431  selberg3lem2  26439  pntrsumo1  26446  pnt2  26494  pnt  26495  axcontlem2  27056  usgrexmplef  27347  griedg0ssusgr  27353  nbgrssvtx  27430  nbgrssovtx  27449  uvtxssvtx  27478  rgrusgrprc  27677  clwlkswks  27863  wwlkssswrd  27946  wwlkssswwlksn  27950  wspthsswwlkn  28002  wspthsswwlknon  28005  clwwlksclwwlkn  28114  phrel  28896  bnrel  28948  hlrel  28971  shex  29293  chsssh  29306  hhssnv  29345  choc1  29408  shunssi  29449  shsleji  29451  shsub1i  29453  shsub2i  29454  shsidmi  29465  omlsii  29484  spanuni  29625  spansni  29638  5oalem7  29741  3oalem3  29745  pjrni  29783  mayete3i  29809  hmopex  29956  cnlnssadj  30161  adjbdln  30164  adjsslnop  30168  shatomistici  30442  hatomistici  30443  xrge0tsmsd  31036  primefldchr  31212  esumpcvgval  31758  hashf2  31764  insiga  31817  sigapisys  31835  sigaldsys  31839  sigapildsys  31842  sxbrsigalem0  31950  dya2icobrsiga  31955  sxbrsigalem1  31964  sxbrsigalem2  31965  eulerpartlemb  32047  chtvalz  32321  logdivsqrle  32342  bnj1398  32727  bnj1498  32754  fineqvacALT  32780  erdszelem9  32874  erdsze2lem2  32879  kur14lem9  32889  ptpconn  32908  iinllyconn  32929  cvmlift3  33003  mppsthm  33254  madef  33777  imagesset  33992  altxpsspw  34016  topjoin  34291  onsstopbas  34355  onsucconni  34363  onintopssconn  34366  onint1  34375  oninhaus  34376  bj-snglss  34897  bj-imdirco  35096  bj-modssabl  35186  bj-rvecssmod  35201  bj-rvecssvec  35206  bj-rvecsscmod  35208  icoreunrn  35267  difunieq  35282  poimirlem8  35522  poimirlem18  35532  poimirlem21  35535  poimirlem22  35536  poimirlem31  35545  poimirlem32  35546  heiborlem3  35708  atssbase  37041  eldioph3b  40290  diophin  40297  diophun  40298  eldiophss  40299  isnumbasabl  40634  isnumbasgrp  40635  dfacbasgrp  40636  mon1psubm  40734  inintabss  40862  intimass  40939  inaex  41588  nzin  41609  unipwrVD  42125  unipwr  42126  supxrre3  42537  fsumiunss  42791  rrpsscn  42804  dvnmul  43159  dvnprodlem2  43163  stoweidlem34  43250  stirlinglem13  43302  fourierdlem20  43343  fourierdlem62  43384  fourierdlem83  43405  fourierdlem101  43423  fourierdlem103  43425  fourierdlem104  43426  fourierdlem111  43433  fouriersw  43447  qndenserrnbllem  43510  sge0iunmptlemre  43628  nn0ssge0  43637  sge0isum  43640  sge0seq  43659  sge0reuz  43660  caragendifcl  43727  carageniuncllem2  43735  hoicvrrex  43769  smfaddlem1  43970  smfaddlem2  43971  mbfpsssmf  43990  ringssrng  45111  srhmsubc  45307  srhmsubcALTV  45325  lvecpsslmod  45521  thincssc  45980  aacllem  46176  amgmwlem  46177  amgmlemALT  46178