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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ssid  4005  ssv  4007  ssrab2  4078  difss  4132  ssun1  4173  inss1  4229  0ss  4397  difprsnss  4803  snsspw  4846  uniin  4936  pwuni  4950  iuniin  5010  iunpwss  5111  relopabi  5823  dmin  5912  dmrnssfld  5970  dmcoss  5971  dminss  6153  imainss  6154  fvssunirn  6925  fviss  6969  opabresex2  7461  fvmptopab  7463  mapfoss  8846  fsetsspwxp  8847  mapsspm  8870  pmsspw  8871  uniixp  8915  pwfilem  9177  pwfilemOLD  9346  dffi3  9426  dfom3  9642  onwf  9825  tcrank  9879  djuss  9915  djuunxp  9916  djuun  9921  cardprclem  9974  alephsson  10095  ackbij1  10233  cardcf  10247  cfeq0  10251  dfacfin7  10394  hsmexlem6  10426  canthnum  10644  inaprc  10831  nqerf  10925  addnqf  10943  mulnqf  10944  dmrecnq  10963  reclem2pr  11043  wuncn  11165  zssre  12565  zsscn  12566  nnssz  12580  elq  12934  zssq  12940  qssre  12943  ixxssixx  13338  iooval2  13357  ioossre  13385  rge0ssre  13433  fzssz  13503  fz1ssnn  13532  fzssuz  13542  fzssp1  13544  uzdisj  13574  fz0ssnn0  13596  nn0disj  13617  fzossfz  13651  fzouzsplit  13667  fzo0ssnn0  13713  uzrdgfni  13923  seqcoll  14425  wrdexb  14475  fclim  15497  isercolllem3  15613  climcnds  15797  divcnv  15799  harmonic  15805  bitsss  16367  prmssnn  16613  maxprmfct  16646  1arith  16860  4sqlem19  16896  vdwlem12  16925  restsspw  17377  mremre  17548  mreacs  17602  isfunc  17814  homarel  17986  ledm  18543  lern  18544  smndex1basss  18786  sgrpssmgm  18814  mndsssgrp  18815  prdsgrpd  18933  prdsinvgd  18934  symgpssefmnd  19263  symgsubmefmndALT  19271  pgrpsubgsymg  19277  symgtrf  19337  odf1o2  19441  sylow3lem3  19497  sylow3lem6  19500  oppglsm  19510  efgsfo  19607  0frgp  19647  prdscmnd  19729  prdsabld  19730  dprdssv  19886  dprdres  19898  prdsringd  20134  prdscrngd  20135  unitss  20190  subrgint  20342  subdrgint  20419  sdrgint  20420  primefld  20421  lssintcl  20575  prdslmodd  20580  xrge0subm  20986  cnsubmlem  20993  cnsubglem  20994  cnsubdrglem  20996  cnmsubglem  21008  zringunit  21036  zringlpir  21037  znf1o  21107  ocvss  21223  dsmmsubg  21298  dsmmlss  21299  lbslinds  21388  unitg  22470  cldss2  22534  indiscld  22595  iscldtop  22599  llyssnlly  22982  llyidm  22992  nllyidm  22993  toplly  22994  hauslly  22996  lly1stc  23000  dissnref  23032  txindis  23138  pthaus  23142  ptcmpfi  23317  ufinffr  23433  cnflf2  23507  flimfcls  23530  alexsubALTlem3  23553  ptcmplem1  23556  ptcmpg  23561  prdstmdd  23628  prdstgpd  23629  ust0  23724  prdsms  24040  qdensere  24286  blssioo  24311  tgioo  24312  xrtgioo  24322  xrsmopn  24328  zdis  24332  reperflem  24334  xrge0gsumle  24349  xrge0tsms  24350  icopnfhmeo  24459  bndth  24474  voliunlem2  25068  voliunlem3  25069  vitali  25130  ismbf3d  25171  itg2seq  25260  limccl  25392  limcresi  25402  dvef  25497  aasscn  25831  qssaa  25837  aannenlem2  25842  aannenlem3  25843  ulmcn  25911  mtestbdd  25917  iblulm  25919  reeff1o  25959  reefgim  25962  efifo  26056  dfrelog  26074  relogf1o  26075  logdmss  26150  logcn  26155  dvloglem  26156  logf1o2  26158  dvlog  26159  dvlog2lem  26160  dvlog2  26161  logtayl  26168  cxpcn  26253  cxpcn2  26254  cxpcn3  26256  resqrtcn  26257  efrlim  26474  dfef2  26475  cxp2lim  26481  basellem3  26587  basellem4  26588  sqff1o  26686  dchrmhm  26744  chtppilim  26978  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  dchrisumlema  26991  selberg2lem  27053  selberg3lem2  27061  pntrsumo1  27068  pnt2  27116  pnt  27117  madef  27351  axcontlem2  28223  usgrexmplef  28516  griedg0ssusgr  28522  nbgrssvtx  28599  nbgrssovtx  28618  uvtxssvtx  28647  rgrusgrprc  28846  clwlkswks  29033  wwlkssswrd  29116  wwlkssswwlksn  29120  wspthsswwlkn  29172  wspthsswwlknon  29175  clwwlksclwwlkn  29284  phrel  30068  bnrel  30120  hlrel  30143  shex  30465  chsssh  30478  hhssnv  30517  choc1  30580  shunssi  30621  shsleji  30623  shsub1i  30625  shsub2i  30626  shsidmi  30637  omlsii  30656  spanuni  30797  spansni  30810  5oalem7  30913  3oalem3  30917  pjrni  30955  mayete3i  30981  hmopex  31128  cnlnssadj  31333  adjbdln  31336  adjsslnop  31340  shatomistici  31614  hatomistici  31615  xrge0tsmsd  32209  primefldchr  32399  1fldgenq  32412  esumpcvgval  33076  hashf2  33082  insiga  33135  sigapisys  33153  sigaldsys  33157  sigapildsys  33160  sxbrsigalem0  33270  dya2icobrsiga  33275  sxbrsigalem1  33284  sxbrsigalem2  33285  eulerpartlemb  33367  chtvalz  33641  logdivsqrle  33662  bnj1398  34045  bnj1498  34072  fineqvacALT  34098  erdszelem9  34190  erdsze2lem2  34195  kur14lem9  34205  ptpconn  34224  iinllyconn  34245  cvmlift3  34319  mppsthm  34570  imagesset  34925  altxpsspw  34949  gg-cxpcn  35184  topjoin  35250  onsstopbas  35314  onsucconni  35322  onintopssconn  35325  onint1  35334  oninhaus  35335  bj-snglss  35851  bj-imdirco  36071  bj-modssabl  36161  bj-rvecssmod  36177  bj-rvecssvec  36182  bj-rvecsscmod  36184  icoreunrn  36240  difunieq  36255  poimirlem8  36496  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  poimirlem31  36519  poimirlem32  36520  heiborlem3  36681  atssbase  38160  eldioph3b  41503  diophin  41510  diophun  41511  eldiophss  41512  isnumbasabl  41848  isnumbasgrp  41849  dfacbasgrp  41850  mon1psubm  41948  omssrncard  42291  inintabss  42329  intimass  42405  inaex  43056  nzin  43077  unipwrVD  43593  unipwr  43594  supxrre3  44035  fsumiunss  44291  rrpsscn  44304  dvnmul  44659  dvnprodlem2  44663  stoweidlem34  44750  stirlinglem13  44802  fourierdlem20  44843  fourierdlem62  44884  fourierdlem83  44905  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fouriersw  44947  qndenserrnbllem  45010  sge0iunmptlemre  45131  nn0ssge0  45140  sge0isum  45143  sge0seq  45162  sge0reuz  45163  caragendifcl  45230  carageniuncllem2  45238  hoicvrrex  45272  smfaddlem1  45479  smfaddlem2  45480  mbfpsssmf  45499  upwordsseti  45599  ringssrng  46656  prdsrngd  46677  subrngint  46739  srhmsubc  46974  srhmsubcALTV  46992  lvecpsslmod  47188  thincssc  47646  aacllem  47848  amgmwlem  47849  amgmlemALT  47850