Theorem ssriv 3987

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951

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

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

This theorem is referenced by:  ssid  4006  ssv  4008  ssrab2  4080  difss  4136  ssun1  4178  inss1  4237  0ss  4400  difprsnss  4799  snsspw  4844  uniin  4931  pwuni  4945  iuniin  5004  iunpwss  5107  relopabi  5832  dmin  5922  dmrnssfld  5984  dmcoss  5985  dminss  6173  imainss  6174  fvssunirn  6939  fviss  6986  opabresex2  7485  fvmptopab  7487  mapfoss  8892  fsetsspwxp  8893  mapsspm  8916  pmsspw  8917  uniixp  8961  pwfilem  9356  dffi3  9471  dfom3  9687  onwf  9870  tcrank  9924  djuss  9960  djuunxp  9961  djuun  9966  cardprclem  10019  alephsson  10140  ackbij1  10277  cardcf  10292  cfeq0  10296  dfacfin7  10439  hsmexlem6  10471  canthnum  10689  inaprc  10876  nqerf  10970  addnqf  10988  mulnqf  10989  dmrecnq  11008  reclem2pr  11088  wuncn  11210  zssre  12620  zsscn  12621  nnssz  12635  elq  12992  zssq  12998  qssre  13001  ixxssixx  13401  iooval2  13420  ioossre  13448  rge0ssre  13496  fzssz  13566  fz1ssnn  13595  fzssuz  13605  fzssp1  13607  uzdisj  13637  fz0ssnn0  13662  nn0disj  13684  fzossfz  13718  fzouzsplit  13734  fzo0ssnn0  13785  uzrdgfni  13999  seqcoll  14503  wrdexb  14563  fclim  15589  isercolllem3  15703  climcnds  15887  divcnv  15889  harmonic  15895  bitsss  16463  prmssnn  16713  maxprmfct  16746  1arith  16965  4sqlem19  17001  vdwlem12  17030  restsspw  17476  mremre  17647  mreacs  17701  isfunc  17909  homarel  18081  ledm  18635  lern  18636  smndex1basss  18918  sgrpssmgm  18946  mndsssgrp  18947  prdsgrpd  19068  prdsinvgd  19069  symgpssefmnd  19413  symgsubmefmndALT  19421  pgrpsubgsymg  19427  symgtrf  19487  odf1o2  19591  sylow3lem3  19647  sylow3lem6  19650  oppglsm  19660  efgsfo  19757  0frgp  19797  prdscmnd  19879  prdsabld  19880  dprdssv  20036  dprdres  20048  prdsrngd  20173  ringssrng  20283  prdsringd  20318  prdscrngd  20319  unitss  20376  subrngint  20560  subrgint  20595  srhmsubc  20680  subdrgint  20804  sdrgint  20805  primefld  20806  lssintcl  20962  prdslmodd  20967  xrge0subm  21425  cnsubmlem  21432  cnsubglem  21433  cnsubdrglem  21436  cnmsubglem  21448  zringunit  21477  zringlpir  21478  znf1o  21570  ocvss  21688  dsmmsubg  21763  dsmmlss  21764  lbslinds  21853  unitg  22974  cldss2  23038  indiscld  23099  iscldtop  23103  llyssnlly  23486  llyidm  23496  nllyidm  23497  toplly  23498  hauslly  23500  lly1stc  23504  dissnref  23536  txindis  23642  pthaus  23646  ptcmpfi  23821  ufinffr  23937  cnflf2  24011  flimfcls  24034  alexsubALTlem3  24057  ptcmplem1  24060  ptcmpg  24065  prdstmdd  24132  prdstgpd  24133  ust0  24228  prdsms  24544  qdensere  24790  blssioo  24816  tgioo  24817  xrtgioo  24828  xrsmopn  24834  zdis  24838  reperflem  24840  xrge0gsumle  24855  xrge0tsms  24856  icopnfhmeo  24974  bndth  24990  voliunlem2  25586  voliunlem3  25587  vitali  25648  ismbf3d  25689  itg2seq  25777  limccl  25910  limcresi  25920  dvef  26018  aasscn  26360  qssaa  26366  aannenlem2  26371  aannenlem3  26372  ulmcn  26442  mtestbdd  26448  iblulm  26450  reeff1o  26491  reefgim  26494  efifo  26589  dfrelog  26607  relogf1o  26608  logdmss  26684  logcn  26689  dvloglem  26690  logf1o2  26692  dvlog  26693  dvlog2lem  26694  dvlog2  26695  logtayl  26702  cxpcn  26787  cxpcnOLD  26788  cxpcn2  26789  cxpcn3  26791  resqrtcn  26792  efrlim  27012  efrlimOLD  27013  dfef2  27014  cxp2lim  27020  basellem3  27126  basellem4  27127  sqff1o  27225  dchrmhm  27285  chtppilim  27519  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  dchrisumlema  27532  selberg2lem  27594  selberg3lem2  27602  pntrsumo1  27609  pnt2  27657  pnt  27658  madef  27895  n0ssold  28355  dfnns2  28362  axcontlem2  28980  usgrexmplef  29276  griedg0ssusgr  29282  nbgrssvtx  29359  nbgrssovtx  29378  uvtxssvtx  29407  rgrusgrprc  29607  clwlkswks  29796  wwlkssswrd  29882  wwlkssswwlksn  29886  wspthsswwlkn  29938  wspthsswwlknon  29941  clwwlksclwwlkn  30050  phrel  30834  bnrel  30886  hlrel  30909  shex  31231  chsssh  31244  hhssnv  31283  choc1  31346  shunssi  31387  shsleji  31389  shsub1i  31391  shsub2i  31392  shsidmi  31403  omlsii  31422  spanuni  31563  spansni  31576  5oalem7  31679  3oalem3  31683  pjrni  31721  mayete3i  31747  hmopex  31894  cnlnssadj  32099  adjbdln  32102  adjsslnop  32106  shatomistici  32380  hatomistici  32381  xrge0tsmsd  33065  primefldchr  33303  1fldgenq  33324  zringidom  33579  esumpcvgval  34079  hashf2  34085  insiga  34138  sigapisys  34156  sigaldsys  34160  sigapildsys  34163  sxbrsigalem0  34273  dya2icobrsiga  34278  sxbrsigalem1  34287  sxbrsigalem2  34288  eulerpartlemb  34370  chtvalz  34644  logdivsqrle  34665  bnj1398  35048  bnj1498  35075  fineqvacALT  35112  erdszelem9  35204  erdsze2lem2  35209  kur14lem9  35219  ptpconn  35238  iinllyconn  35259  cvmlift3  35333  mppsthm  35584  imagesset  35954  altxpsspw  35978  topjoin  36366  onsstopbas  36430  onsucconni  36438  onintopssconn  36441  onint1  36450  oninhaus  36451  bj-snglss  36971  bj-imdirco  37191  bj-modssabl  37281  bj-rvecssmod  37297  bj-rvecssvec  37302  bj-rvecsscmod  37304  icoreunrn  37360  difunieq  37375  poimirlem8  37635  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem31  37658  poimirlem32  37659  heiborlem3  37820  atssbase  39291  readvrec2  42391  eldioph3b  42776  diophin  42783  diophun  42784  eldiophss  42785  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120  mon1psubm  43211  omssrncard  43553  inintabss  43591  intimass  43667  inaex  44316  nzin  44337  unipwrVD  44852  unipwr  44853  supxrre3  45336  fsumiunss  45590  rrpsscn  45603  dvnmul  45958  dvnprodlem2  45962  stoweidlem34  46049  stirlinglem13  46101  fourierdlem20  46142  fourierdlem62  46183  fourierdlem83  46204  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fouriersw  46246  qndenserrnbllem  46309  sge0iunmptlemre  46430  nn0ssge0  46439  sge0isum  46442  sge0seq  46461  sge0reuz  46462  caragendifcl  46529  carageniuncllem2  46537  hoicvrrex  46571  smfaddlem1  46778  smfaddlem2  46779  mbfpsssmf  46798  upwordsseti  46900  clnbgrssvtx  47818  srhmsubcALTV  48241  lvecpsslmod  48424  thincssc  49074  aacllem  49320  amgmwlem  49321  amgmlemALT  49322