Theorem ssriv 4012

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

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

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

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

This theorem is referenced by:  ssid  4031  ssv  4033  ssrab2  4103  difss  4159  ssun1  4201  inss1  4258  0ss  4423  difprsnss  4824  snsspw  4869  uniin  4955  pwuni  4969  iuniin  5027  iunpwss  5130  relopabi  5846  dmin  5936  dmrnssfld  5996  dmcoss  5997  dminss  6184  imainss  6185  fvssunirn  6953  fviss  6999  opabresex2  7502  fvmptopab  7504  mapfoss  8910  fsetsspwxp  8911  mapsspm  8934  pmsspw  8935  uniixp  8979  pwfilem  9384  pwfilemOLD  9416  dffi3  9500  dfom3  9716  onwf  9899  tcrank  9953  djuss  9989  djuunxp  9990  djuun  9995  cardprclem  10048  alephsson  10169  ackbij1  10306  cardcf  10321  cfeq0  10325  dfacfin7  10468  hsmexlem6  10500  canthnum  10718  inaprc  10905  nqerf  10999  addnqf  11017  mulnqf  11018  dmrecnq  11037  reclem2pr  11117  wuncn  11239  zssre  12646  zsscn  12647  nnssz  12661  elq  13015  zssq  13021  qssre  13024  ixxssixx  13421  iooval2  13440  ioossre  13468  rge0ssre  13516  fzssz  13586  fz1ssnn  13615  fzssuz  13625  fzssp1  13627  uzdisj  13657  fz0ssnn0  13679  nn0disj  13701  fzossfz  13735  fzouzsplit  13751  fzo0ssnn0  13797  uzrdgfni  14009  seqcoll  14513  wrdexb  14573  fclim  15599  isercolllem3  15715  climcnds  15899  divcnv  15901  harmonic  15907  bitsss  16472  prmssnn  16723  maxprmfct  16756  1arith  16974  4sqlem19  17010  vdwlem12  17039  restsspw  17491  mremre  17662  mreacs  17716  isfunc  17928  homarel  18103  ledm  18660  lern  18661  smndex1basss  18940  sgrpssmgm  18968  mndsssgrp  18969  prdsgrpd  19090  prdsinvgd  19091  symgpssefmnd  19437  symgsubmefmndALT  19445  pgrpsubgsymg  19451  symgtrf  19511  odf1o2  19615  sylow3lem3  19671  sylow3lem6  19674  oppglsm  19684  efgsfo  19781  0frgp  19821  prdscmnd  19903  prdsabld  19904  dprdssv  20060  dprdres  20072  prdsrngd  20203  ringssrng  20309  prdsringd  20344  prdscrngd  20345  unitss  20402  subrngint  20586  subrgint  20623  srhmsubc  20702  subdrgint  20826  sdrgint  20827  primefld  20828  lssintcl  20985  prdslmodd  20990  xrge0subm  21448  cnsubmlem  21455  cnsubglem  21456  cnsubdrglem  21459  cnmsubglem  21471  zringunit  21500  zringlpir  21501  znf1o  21593  ocvss  21711  dsmmsubg  21786  dsmmlss  21787  lbslinds  21876  unitg  22995  cldss2  23059  indiscld  23120  iscldtop  23124  llyssnlly  23507  llyidm  23517  nllyidm  23518  toplly  23519  hauslly  23521  lly1stc  23525  dissnref  23557  txindis  23663  pthaus  23667  ptcmpfi  23842  ufinffr  23958  cnflf2  24032  flimfcls  24055  alexsubALTlem3  24078  ptcmplem1  24081  ptcmpg  24086  prdstmdd  24153  prdstgpd  24154  ust0  24249  prdsms  24565  qdensere  24811  blssioo  24836  tgioo  24837  xrtgioo  24847  xrsmopn  24853  zdis  24857  reperflem  24859  xrge0gsumle  24874  xrge0tsms  24875  icopnfhmeo  24993  bndth  25009  voliunlem2  25605  voliunlem3  25606  vitali  25667  ismbf3d  25708  itg2seq  25797  limccl  25930  limcresi  25940  dvef  26038  aasscn  26378  qssaa  26384  aannenlem2  26389  aannenlem3  26390  ulmcn  26460  mtestbdd  26466  iblulm  26468  reeff1o  26509  reefgim  26512  efifo  26607  dfrelog  26625  relogf1o  26626  logdmss  26702  logcn  26707  dvloglem  26708  logf1o2  26710  dvlog  26711  dvlog2lem  26712  dvlog2  26713  logtayl  26720  cxpcn  26805  cxpcnOLD  26806  cxpcn2  26807  cxpcn3  26809  resqrtcn  26810  efrlim  27030  efrlimOLD  27031  dfef2  27032  cxp2lim  27038  basellem3  27144  basellem4  27145  sqff1o  27243  dchrmhm  27303  chtppilim  27537  chto1lb  27540  chpchtlim  27541  chpo1ub  27542  dchrisumlema  27550  selberg2lem  27612  selberg3lem2  27620  pntrsumo1  27627  pnt2  27675  pnt  27676  madef  27913  n0ssold  28373  dfnns2  28380  axcontlem2  28998  usgrexmplef  29294  griedg0ssusgr  29300  nbgrssvtx  29377  nbgrssovtx  29396  uvtxssvtx  29425  rgrusgrprc  29625  clwlkswks  29812  wwlkssswrd  29895  wwlkssswwlksn  29899  wspthsswwlkn  29951  wspthsswwlknon  29954  clwwlksclwwlkn  30063  phrel  30847  bnrel  30899  hlrel  30922  shex  31244  chsssh  31257  hhssnv  31296  choc1  31359  shunssi  31400  shsleji  31402  shsub1i  31404  shsub2i  31405  shsidmi  31416  omlsii  31435  spanuni  31576  spansni  31589  5oalem7  31692  3oalem3  31696  pjrni  31734  mayete3i  31760  hmopex  31907  cnlnssadj  32112  adjbdln  32115  adjsslnop  32119  shatomistici  32393  hatomistici  32394  xrge0tsmsd  33041  primefldchr  33268  1fldgenq  33289  zringidom  33544  esumpcvgval  34042  hashf2  34048  insiga  34101  sigapisys  34119  sigaldsys  34123  sigapildsys  34126  sxbrsigalem0  34236  dya2icobrsiga  34241  sxbrsigalem1  34250  sxbrsigalem2  34251  eulerpartlemb  34333  chtvalz  34606  logdivsqrle  34627  bnj1398  35010  bnj1498  35037  fineqvacALT  35074  erdszelem9  35167  erdsze2lem2  35172  kur14lem9  35182  ptpconn  35201  iinllyconn  35222  cvmlift3  35296  mppsthm  35547  imagesset  35917  altxpsspw  35941  topjoin  36331  onsstopbas  36395  onsucconni  36403  onintopssconn  36406  onint1  36415  oninhaus  36416  bj-snglss  36936  bj-imdirco  37156  bj-modssabl  37246  bj-rvecssmod  37262  bj-rvecssvec  37267  bj-rvecsscmod  37269  icoreunrn  37325  difunieq  37340  poimirlem8  37588  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem31  37611  poimirlem32  37612  heiborlem3  37773  atssbase  39246  eldioph3b  42721  diophin  42728  diophun  42729  eldiophss  42730  isnumbasabl  43063  isnumbasgrp  43064  dfacbasgrp  43065  mon1psubm  43160  omssrncard  43502  inintabss  43540  intimass  43616  inaex  44266  nzin  44287  unipwrVD  44803  unipwr  44804  supxrre3  45240  fsumiunss  45496  rrpsscn  45509  dvnmul  45864  dvnprodlem2  45868  stoweidlem34  45955  stirlinglem13  46007  fourierdlem20  46048  fourierdlem62  46089  fourierdlem83  46110  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fouriersw  46152  qndenserrnbllem  46215  sge0iunmptlemre  46336  nn0ssge0  46345  sge0isum  46348  sge0seq  46367  sge0reuz  46368  caragendifcl  46435  carageniuncllem2  46443  hoicvrrex  46477  smfaddlem1  46684  smfaddlem2  46685  mbfpsssmf  46704  upwordsseti  46804  clnbgrssvtx  47704  srhmsubcALTV  48048  lvecpsslmod  48236  thincssc  48693  aacllem  48895  amgmwlem  48896  amgmlemALT  48897