Theorem ssriv 3938

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ss 3919

This theorem is used by:  ssid  3956  ssv  3958  ssrab2  4031  difss  4086  ssun1  4127  inss1  4185  0ss  4353  difprsnss  4765  snsspw  4807  uniinOLD  4895  pwuni  4909  iuniin  4967  iunpwss  5071  relopabi  5807  dmin  5899  dmrnssfld  5962  dmcoss  5963  dmcossOLD  5964  dminss  6148  imainss  6149  fvssunirn  6913  fviss  6959  opabresex2  7471  fvmptopab  7472  mapfoss  8857  fsetsspwxp  8858  mapsspm  8887  pmsspw  8888  uniixp  8932  pwfilem  9291  dffi3  9405  dfom3  9630  onwf  9816  tcrank  9870  djuss  9929  djuunxp  9930  djuun  9935  cardprclem  9988  alephsson  10107  ackbij1  10243  cardcf  10257  cfeq0  10262  dfacfin7  10405  hsmexlem6  10437  canthnum  10662  inaprc  10849  nqerf  10943  addnqf  10961  mulnqf  10962  dmrecnq  10981  reclem2pr  11061  wuncn  11183  zssre  12626  zsscn  12627  nnssz  12641  elq  13003  zssq  13009  qssre  13012  ixxssixx  13416  iooval2  13435  ioossre  13464  rge0ssre  13513  fzssz  13584  fz1ssnn  13614  fzssuz  13624  fzssp1  13626  uzdisj  13656  fz0ssnn0  13681  nn0disj  13703  fzossfz  13738  fzouzsplit  13754  fzo0ssnn0  13806  uzrdgfni  14026  seqcoll  14533  wrdexb  14594  fclim  15644  isercolllem3  15758  climcnds  15944  divcnv  15946  harmonic  15952  bitsss  16522  prmssnn  16772  prmssuz2  16793  maxprmfct  16806  1arith  17025  4sqlem19  17061  vdwlem12  17090  restsspw  17522  mremre  17694  mreacs  17752  isfunc  17959  homarel  18131  ledm  18684  lern  18685  chnexg  18712  smndex1basss  19023  sgrpssmgm  19051  mndsssgrp  19052  prdsgrpd  19179  prdsinvgd  19180  symgpssefmnd  19529  symgsubmefmndALT  19536  pgrpsubgsymg  19542  symgtrf  19602  odf1o2  19706  sylow3lem3  19762  sylow3lem6  19765  oppglsm  19775  efgsfo  19872  0frgp  19912  prdscmnd  19994  prdsabld  19995  dprdssv  20151  dprdres  20163  prdsrngd  20317  ringssrng  20433  prdsringd  20467  prdscrngd  20468  unitss  20523  subrngint  20728  subrgint  20763  srhmsubc  20848  subdrgint  20975  sdrgint  20976  primefld  20977  lssintcl  21154  prdslmodd  21159  cnsubmlem  21634  cnsubglem  21635  cnsubdrglem  21637  cnmsubglem  21649  xrge0subm  21662  zringunit  21685  zringlpir  21686  znf1o  21770  ocvss  21889  dsmmsubg  21962  dsmmlss  21963  lbslinds  22052  unitg  23198  cldss2  23261  indiscld  23322  iscldtop  23326  llyssnlly  23710  llyidm  23720  nllyidm  23721  toplly  23722  hauslly  23724  lly1stc  23728  dissnref  23760  txindis  23866  pthaus  23870  ptcmpfi  24045  ufinffr  24161  cnflf2  24235  flimfcls  24258  alexsubALTlem3  24281  ptcmplem1  24284  ptcmpg  24289  prdstmdd  24356  prdstgpd  24357  ust0  24452  prdsms  24763  qdensere  25001  blssioo  25027  tgioo  25028  xrtgioo  25039  xrsmopn  25045  zdis  25049  reperflem  25051  xrge0gsumle  25066  xrge0tsms  25067  icopnfhmeo  25177  bndth  25192  voliunlem2  25785  voliunlem3  25786  vitali  25847  ismbf3d  25888  itg2seq  25976  limccl  26109  limcresi  26119  dvef  26214  aasscn  26557  qssaa  26564  aannenlem2  26572  aannenlem3  26573  ulmcn  26642  mtestbdd  26648  iblulm  26650  reeff1o  26690  reefgim  26693  efifo  26792  dfrelog  26810  relogf1o  26811  logdmss  26887  logcn  26892  dvloglem  26893  logf1o2  26895  dvlog  26896  dvlog2lem  26897  dvlog2  26898  logtayl  26905  cxpcn  26990  cxpcn2  26991  cxpcn3  26993  resqrtcn  26994  efrlim  27214  dfef2  27215  cxp2lim  27221  basellem3  27327  basellem4  27328  sqff1o  27426  dchrmhm  27485  chtppilim  27719  chto1lb  27722  chpchtlim  27723  chpo1ub  27724  dchrisumlema  27732  selberg2lem  27794  selberg3lem2  27802  pntrsumo1  27809  pnt2  27857  pnt  27858  madef  28109  oniso  28544  bdayn0sf1o  28643  dfnns2  28645  axcontlem2  29430  usgrexmplef  29727  griedg0ssusgr  29733  nbgrssvtx  29810  nbgrssovtx  29829  uvtxssvtx  29858  rgrusgrprc  30057  clwlkswks  30250  wwlkssswrd  30338  wwlkssswwlksn  30342  wspthsswwlkn  30394  wspthsswwlknon  30397  clwwlksclwwlkn  30509  phrel  31304  bnrel  31356  hlrel  31379  shex  31701  chsssh  31714  hhssnv  31753  choc1  31816  shunssi  31857  shsleji  31859  shsub1i  31861  shsub2i  31862  shsidmi  31873  omlsii  31892  spanuni  32033  spansni  32046  5oalem7  32149  3oalem3  32153  pjrni  32191  mayete3i  32217  hmopex  32364  cnlnssadj  32569  adjbdln  32572  adjsslnop  32576  shatomistici  32850  hatomistici  32851  xrge0tsmsd  33521  primefldchr  33750  1fldgenq  33771  zringidom  33969  esumpcvgval  34596  hashf2  34602  insiga  34656  sigapisys  34674  sigaldsys  34678  sigapildsys  34681  sxbrsigalem0  34790  dya2icobrsiga  34795  sxbrsigalem1  34804  sxbrsigalem2  34805  eulerpartlemb  34887  chtvalz  35145  logdivsqrle  35166  bnj1398  35551  bnj1498  35578  r1omfi  35621  fineqvacALT  35651  erdszelem9  35786  erdsze2lem2  35791  kur14lem9  35801  ptpconn  35820  iinllyconn  35841  cvmlift3  35915  mppsthm  36166  imagesset  36540  altxpsspw  36565  topjoin  36992  onsstopbas  37056  onsucconni  37064  onintopssconn  37067  onint1  37076  oninhaus  37077  ttcid  37119  dfttc4lem2  37156  dfttc4  37157  bj-snglss  37722  bj-imdirco  37950  bj-modssabl  38040  bj-rvecssmod  38056  bj-rvecssvec  38061  bj-rvecsscmod  38063  icoreunrn  38121  difunieq  38136  poimirlem8  38385  poimirlem18  38395  poimirlem21  38398  poimirlem22  38399  poimirlem31  38408  poimirlem32  38409  heiborlem3  38571  disjsssrels  39692  atssbase  40171  readvrec2  43244  eldioph3b  43618  diophin  43625  diophun  43626  eldiophss  43627  isnumbasabl  43955  isnumbasgrp  43956  dfacbasgrp  43957  mon1psubm  44048  omssrncard  44388  inintabss  44426  intimass  44502  inaex  45129  nzin  45150  unipwrVD  45662  unipwr  45663  supxrre3  46163  fsumiunss  46413  rrpsscn  46426  dvnmul  46779  dvnprodlem2  46783  stoweidlem34  46870  stirlinglem13  46922  fourierdlem20  46963  fourierdlem62  47004  fourierdlem83  47025  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fouriersw  47067  qndenserrnbllem  47130  sge0iunmptlemre  47251  nn0ssge0  47260  sge0isum  47263  sge0seq  47282  sge0reuz  47283  caragendifcl  47350  carageniuncllem2  47358  hoicvrrex  47392  smfaddlem1  47599  smfaddlem2  47600  mbfpsssmf  47619  wrddun2  47726  chndun2  47731  chnrun2  47736  clnbgrssvtx  48755  srhmsubcALTV  49248  lvecpsslmod  49445  thincssc  50358  aacllem  50780  amgmwlem  50828  amgmlemALT  50829